perm filename PROVE2.NEW[1,JRA]4 blob
sn#030167 filedate 1973-03-13 generic text, type T, neo UTF8
00100
00200
00300 (DEFPROP NEWPROOF
00400 (NIL NEWPROOF
00500 ALLPOS
00600 ALLNEG
00700 ANCESTOR
00800 SEARCH1
00900 CONST
01000 HERE
01100 VAR
01200 ISCLS
01300 ISCL
01400 ISLIT
01500 ISTRM
01600 MKWRD
01700 NEG
01800 NEGBIT
01900 POS
02000 POSBIT
02100 SEARCH
02200 NUM
02300 NEGL
02400 APPENDIT
02500 ANDOR
02600 ASSOC1
02700 ATTEMPT
02800 AUTO
02900 BAKSUB
03000 BOOKEEP
03100 BUILTED
03200 BUILTED1
03300 BUILTCH
03400 BUILTCH1
03500 CHOICE
03600 CHOICE1
03700 CLAUSES
03800 CLAUSES2
03900 CLAUSES1
04000 CNF
04100 CNF1
04200 CNF2
04300 CNF3
04400 CNVT
04500 CNVT2
04600 CNVT3
04700 COPY
04800 COPYDELETED
04900 *CL
05000 DEMOD
05100 DEM
05200 DEPTH
05300 DEPTH1
05400 DEL
05500 DOML
05600 DOMC
05700 DOWN
05800 EDIT
05900 ERPRINT
06000 ERPRIN1
06100 EXPUNGE
06200 FINI
06300 FIXNEG
06400 FIXQFF
06500 FIXQFF1
06600 GENSKOLEM
06700 GETNAME
06800 GETTERMS
06900 GETVARS
07000 GOLIST
07100 INCLAUSES
07200 INITIAL
07300 INITIALAX
07400 INITIALAX1
07500 MAKVAR
07600 MAKOVAR
07700 MAPIT
07800 MATCHER
07900 MATCH1
08000 MATCHTR
08100 MATCHPN
08200 MATMLT
08300 MATMLT*
08400 MAX
08450 MAXDEPTH MAXDEPTH1 MAXLENGTH
08500 MEMC
08600 MIN1
08700 MINIMIZE
08800 MIN
08900 MKSYM
09000 MODEL
09100 NCONC1
09200 NEGATE
09300 NEGSGN
09400 NOSYM
09500 OCR
09600 OCR1
09700 ONEGSGN
09800 *NOPOINT
09900 OCCUR
10000 ORDER
10100 ORDEREQUAL
10200 PARMOD
10300 PARMOD1
10400 POTZ
10500 PRECNF
10600 PROOF1
10700 PROVE
10800 PRPAR
10900 PRFPRINT
11000 PRFPR1
11100 PROOF
11200 PTRS
11300 PUNIFY
11400 QUERY
11500 REAL-LNGTH
11600 REDUCER
11700 RESOLVE
11800 RESOLVE1
11900 RESUNITP
12000 RESUNITN
12100 RESET
12200 RESET1
12300 SET1
12400 SET2
12500 SET3
12600 SETUP
12700 SEARCH2
12800 S2
12900 SETQUERY
13000 SETQUERY1
13100 SETQUERY2
13200 SETSUP
13300 SUBS3TA
13400 SUBS3T**
13500 SUB*
13600 SUBSKOL
13700 SUPPORT
13800 SUBSUME1
13900 SUBS2T
14000 SUBS3T
14100 SUBSUME
14200 SUBSUME*
14300 SUBST1
14400 TCOPY
14500 TERMS
14600 TERMS1
14700 TERMS2
14800 TIMEIT
14900 TREE
15000 TREEDEP
15100 TRY
15200 TRY1
15300 TRYIT
15400 TRAVERSE
15500 UNIT
15600 UNITS
15700 UNITRES
15800 UNITREDUCT
15900 UNITPN
16000 UNIFY
16100 UNI
16200 UNION
16300 UNWIND
16400 UPDATE
16500 UPGETL
16600 UPGETL1
16700 UPGETNU
16800 UPDATESTATE
16900 UPIT
17000 UPIT1
17100 UP1A
17200 UP1B
17300 VARIT
17400 VINE
17500 <)
17600 VALUE)
17700
17800 (DEFPROP ALLPOS
17900 (LAMBDA (C) (LIST (QUOTE NULL) (LIST (QUOTE CADAR) (CADR C))))
18000 MACRO)
18100
18200 (DEFPROP ALLNEG
18300 (LAMBDA (C) (LIST (QUOTE EQ) (LIST (QUOTE CADAR) (CADR C)) (LIST (QUOTE CDR) (CADR C))))
18400 MACRO)
18500
18600 (DEFPROP ANCESTOR
18700 (LAMBDA (X) (LIST (QUOTE CDDDAR) (CADR X)))
18800 MACRO)
18900
19000 (DEFPROP SEARCH1
19100 (LAMBDA (X) (LIST (QUOTE SEARCH2) (CADR X) (CADDR X) NIL))
19200 MACRO)
19300
19400 (DEFPROP CONST
19500 (LAMBDA (X) (LIST (QUOTE NULL) (LIST (QUOTE CDR) (CADR X))))
19600 MACRO)
19700
19800 (DEFPROP HERE
19900 (LAMBDA (X) (LIST (QUOTE CAAR) (CADR X)))
20000 MACRO)
20100
20200 (DEFPROP VAR
20300 (LAMBDA (L) (LIST (QUOTE NUMBERP) (CADR L)))
20400 MACRO)
20500
20600 (DEFPROP ISCLS
20700 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 1))
20800 MACRO)
20900
21000 (DEFPROP ISCL
21100 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 2))
21200 MACRO)
21300
21400 (DEFPROP ISLIT
21500 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 3))
21600 MACRO)
21700
21800 (DEFPROP ISTRM
21900 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 4))
22000 MACRO)
22100
22200 (DEFPROP MKWRD
22300 (LAMBDA (L) (LIST (QUOTE CDDAR) (CADR L)))
22400 MACRO)
22500
22600 (DEFPROP NEG
22700 (LAMBDA (X) (LIST (QUOTE EQ) (QUOTE ESCAPE) (LIST (QUOTE CAR) (CADR X))))
22800 MACRO)
22900
23000 (DEFPROP NEGBIT
23100 (LAMBDA (X) (LIST (QUOTE CDDAAR) (CADR X)))
23200 MACRO)
23300
23400 (DEFPROP POS
23500 (LAMBDA (X) (LIST (QUOTE NOT) (LIST (QUOTE NEG) (CADR X))))
23600 MACRO)
23700
23800 (DEFPROP POSBIT
23900 (LAMBDA (X) (LIST (QUOTE CADAAR) (CADR X)))
24000 MACRO)
24100
24200 (DEFPROP SEARCH
24300 (LAMBDA (X) (LIST (QUOTE SEARCH2) (CADR X) (CADDR X) (CADR X)))
24400 MACRO)
24500
24600 (DEFPROP NUM
24700 (LAMBDA (C) (LIST (QUOTE CAAAR) (CADR C)))
24800 MACRO)
24900
25000 (DEFPROP NEGL
25100 (LAMBDA (C) (LIST (QUOTE CADAR) (CADR C)))
25200 MACRO)
25300
25400 (DEFPROP APPENDIT
25500 (LAMBDA(X Y)
25600 (PROG NIL (COND (USINGFL (SETQ USING (CONS N2 (APPEND (REVERSE Y) USING))))) (RETURN (APPEND X Y))))
25700 EXPR)
25800
25900 (DEFPROP ANDOR
26000 (LAMBDA(C UNL EXL PF)
26100 (PROG (Z1 Z2)
26200 (SETQ Z1 (CADR C))
26300 (SETQ Z2 (CADDR C))
26400 (COND
26500 ((OR (AND (EQ (CAR C) (QUOTE AND)) PF) (AND (EQ (CAR C) (QUOTE OR)) (NOT PF)))
26600 (RETURN (LIST (QUOTE AND) Z1 Z2)))
26700 ((EQ (CAR Z1) (QUOTE AND))
26800 (RETURN
26900 (LIST (QUOTE AND)
27000 (CNF1 (LIST (QUOTE OR) (CADR Z1) Z2) UNL EXL T)
27100 (CNF1 (LIST (QUOTE OR) (CADDR Z1) (COPY Z2)) UNL EXL T))))
27200 ((EQ (CAR Z2) (QUOTE AND))
27300 (RETURN
27400 (LIST (QUOTE AND)
27500 (CNF1 (LIST (QUOTE OR) (CADR Z2) (COPY Z1)) UNL EXL T)
27600 (CNF1 (LIST (QUOTE OR) (CADDR Z2) Z1) UNL EXL T))))
27700 (T (RETURN (LIST (QUOTE OR) Z1 Z2))))))
27800 EXPR)
27900
28000 (DEFPROP ASSOC1
28100 (LAMBDA (X L) (COND ((NULL L) NIL) ((EQ (CDR X) (CDAAR L)) (CAR L)) (T (ASSOC1 X (CDR L)))))
28200 EXPR)
28300
28400 (DEFPROP ATTEMPT
28500 (LAMBDA(Z S C)
28600 (PROG (NEWNAME SUPPORT
28700 EDITSTRAT
28800 LCL
28900 LVL
29000 CNT
29100 LSTCLS
29200 LLST
29300 Z1
29400 MERGE
29500 ORDER
29600 DEBUG
29700 DEPTH
29800 LENGTH
29900 ANCESTRY
30000 STRATEGY
30100 STRAT
30200 PMODEL
30300 NMODEL
30400 PFLG
30500 PDEPTH
30600 DLIST
30700 XYZ
30800 XYZ1
30900 COND
31000 UNAXP
31100 UNAXN
31200 SAT
31300 EE
31400 EE1
31500 CLAUSES
31600 SUBCLAUSES
31700 COUNT)
31800 (SETQ TBL (SET1 (APPEND PREFN INFN)))
31900 (SET3 Z)
32000 (SETQ Z (MINIMIZE Z))
32100 (SETQ NEWNAME (INITIAL Z))
32200 (SETQ CLAUSES Z)
32300 (UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
32400 (SETQ COND C)
32500 (SETQ LVL 1)
32600 (SETQ COUNT 0)
32700 (SETQ Z (UNITPN Z))
32800 (SETQ UNAXP (CAR Z))
32900 (SETQ UNAXN (CDR Z))
33000 (COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
33100 (SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
33200 (T (SETQ SUBCLAUSES CLAUSES)))
33300 (SETQ LCL (LAST CLAUSES))
33400 (SETQ LSTCLS LCL)
33500 (SETQ XYZ (SETQ EE CLAUSES))
33600 (SETQ EE1 (LAST CLAUSES))
33700 BB (SETQ LLST (CONS (CAR XYZ) LLST))
33800 (SETQ XYZ (CDR XYZ))
33900 (COND (XYZ (GO BB)))
34000 (SETQ Z1 (ERRSET (TRYIT)))
34100 (COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (SETQUERY1 CLAUSES STRAT)))
34200 ((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
34300 (EVAL
34400 (LIST (QUOTE OUTC)
34500 (LIST (QUOTE OUTPUT)
34600 (QUOTE PRF)
34700 (QUOTE DSK:)
34800 (CONS (READLIST
34900 (CONS (QUOTE N)
35000 (CONS (SETQ PRNO (ADD1 PRNO))
35100 FILENAM)))
35200 (QUOTE PRF)))
35300 NIL)))
35400 (QUERY)
35500 (PROOF LHP RHP)
35600 (OUTC Z T)
35700 (RETURN Z1))
35800 (T (RETURN Z1)))))
35900 EXPR)
36000
36100 (DEFPROP AUTO
36200 (LAMBDA(XX)
36300 (PROG (X1 Z2 D M STRATEGY SUPPORT EDITSTRAT MERGE ORDER DEBUG ANCESTRY PMODEL NMODEL PFLG PDEPTH DLIST)
36400 (COND (EQUAL (SETQ PFLG NIL)) (T (SETQ PFLG NIL)))
36500 (SETQ PDEPTH 3)
36600 (SETQ DDEPTH 4)
36700 (SETQ X1 XX)
36800 (SETQ M (SETQ D 0))
36900 A (SETQ M (MAX M (LENGTH (CDAR X1))))
37000 (SETQ D (MAX D (DEPTH (CDAR X1))))
37100 (SETQ Z2 (CAR X1))
37200 (COND
37300 ((AND (EQ (LENGTH (CDR Z2)) 1) (EQ (CAADR Z2) EQUAL) (NOT (EQ (CADADR Z2) (CAR (CDDADR Z2)))))
37400 (SETQ DLIST (CONS (CONS (CONS (CAAAR Z2) (CDAR Z2)) (CDR Z2)) DLIST))))
37500 (SETQ X1 (CDR X1))
37600 (COND ((CDR X1) (GO A)))
37700 (SETQ Z2 (ASSOC THEOREMNAME NEWNAME))
37800 (COND ((NULL Z2) (GO C)) (T (SETQ Z2 (CDR Z2))))
37900 B (COND (Z2 (SETQ SUPPORT (CONS (CDAR Z2) SUPPORT)) (SETQ Z2 (CDR Z2)) (GO B)))
38000 C (COND ((NULL LENGTH) (SETQ LENGTH (DIFFERENCE (PLUS M (LENGTH (CDAR X1))) 2)))
38100 ((ZEROP ITER) (SETQ LENGTH (ADD1 LENGTH))))
38200 (COND ((NOT (GREATERP LENGTH 0)) (SETQ LENGTH 1)))
38300 (COND ((NULL DEPTH) (SETQ DEPTH (ADD1 D))) ((NOT (ZEROP ITER)) (SETQ DEPTH (ADD1 DEPTH))))
38400 (COND ((ZEROP ITER) (SETQ ITER 1)) (T (SETQ ITER 0)))
38500 (COND (SUPPORT (SETQ STRATEGY (QUOTE (LAMBDA (C1 C2) (OR (SUPPORT C2) (SUPPORT C1)))))
38600 (SETQ SAVESTR (QUOTE (AND ANCESTRY (SUPPORT THEOREM)))))
38700 (T (SETQ SAVESTR (QUOTE ANCESTRY))))
38800 (SETQ ANCESTRY T)
38900 (SETQ EDITSTRAT
39000 (LIST @LAMBDA @(C)(LIST @OR (LIST @MAXDEPTH @(CDR C) DEPTH)
39050 (LIST @MAXLENGTH @C LENGTH))))
39100 (SETQ SAVEED(CAR(LAST EDITSTRAT)))
39200 (SETQ DEBUG T)
39300 (COND (DLIST (SET3 DLIST)))
39400 (COND
39500 (EQUAL (SETQ SAVESTR (CONS (QUOTE AND) (CONS SAVESTR (LIST (LIST (QUOTE EQUALITY) EQUAL PDEPTH)))))))
39600 (RETURN
39700 (LIST STRATEGY
39800 SUPPORT
39900 EDITSTRAT
40000 MERGE
40100 ORDER
40200 DEBUG
40300 DEPTH
40400 LENGTH
40500 ANCESTRY
40600 PMODEL
40700 NMODEL
40800 PFLG
40900 EQUAL
41000 PDEPTH
41100 DLIST))))
41200 EXPR)
41300
41400 (DEFPROP AUTO
41500 (NIL . T)
41600 VALUE)
41700
41800 (DEFPROP BAKSUB
41900 (LAMBDA(L R)
42000 (PROG (Z U1 U4)
42100 (SETQ Z L)
42200 ED4 (COND ((NOT Z) (RETURN NIL)) ((OR (NOT (HERE (CAR Z))) (ATOM (CDR (ANCESTOR (CAR Z))))) (GO ED6A)))
42300 (SETQ U1 R)
42400 ED3 (SETQ U4 (CAR Z))
42500 ED1 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
42600 ED6 (SETQ U1 (CDR U1))
42700 (COND (U1 (GO ED1)))
42800 ED6A (SETQ Z (CDR Z))
42900 (GO ED4)
43000 ED2 (DEL U4)
43100 (GO ED4)))
43200 EXPR)
43300
43400 (DEFPROP BOOKEEP
43500 (LAMBDA(L M N)
43600 (PROG (U)
43700 B1 (SETQ U M)
43800 B3 (RPLACD (CDAAR U) (CONS 0 N))
43900 (SETQ U (CDR U))
44000 (COND ((NULL U) (RETURN (NCONC L M))))
44100 (GO B3)))
44200 EXPR)
44300
44400 (DEFPROP BUILTED
44500 (LAMBDA (X) (LIST (QUOTE LAMBDA) (QUOTE (C)) (BUILTED1 X)))
44600 EXPR)
44700
44800 (DEFPROP BUILTED1
44900 (LAMBDA(X)
45000 (COnD ((ATOM X) X)
45100 ((ATOM (CAR X))
45200 (COND ((EQ (CAR X) (QUOTE DEMOD)) (SETQ DDEPTH (CADDR X)) (SETQ DLIST (*CL (CADR X))) NIL)
45300 (T (CONS (CAR X) (BUILTED1 (CDR X))))))
45400 ((EQ (CAAR X) (QUOTE DEMOD)) (SETQ DDEPTH (CADDAR X)) (SETQ DLIST (*CL (CADAR X))) (BUILTED1 (CDR X)))
45500 (T (CONS (BUILTED1 (CAR X)) (BUILTED1 (CDR X))))))
45600 EXPR)
45700
45800 (DEFPROP BUILTCH
45900 (LAMBDA(X)
46000 (PROG (Z)
46100 (SETQ Z (BUILTCH1 X))
46200 (RETURN
46300 (COND ((OR (ATOM Z) (EQUAL Z (QUOTE (AND))) (EQUAL X (QUOTE (OR)))) NIL)
46400 (T (LIST (QUOTE LAMBDA) (QUOTE (C1 C2)) Z))))))
46500 EXPR)
46600
46700 (DEFPROP BUILTCH1
46800 (LAMBDA(X)
46900 (COND ((ATOM X)
47000 (COND ((EQ X (QUOTE ANCESTRY)) (SETQ ANCESTRY T) NIL)
47100 ((EQ X (QUOTE NONE)) NIL)
47200 ((MEMQ X (QUOTE (VINE ALLPOS ALLNEG UNIT)))
47300 (LIST (QUOTE OR) (LIST X (QUOTE C1)) (LIST X (QUOTE C2))))
47400 (T X)))
47500 ((EQ (CAR X) (QUOTE SUPPORT)) (SETSUP (CDR X)) (QUOTE (SUPPORT C2)))
47600 ((EQ (CAR X) (QUOTE MODEL)) (SETQ PMODEL (CADR X))
47700 (SETQ NMODEL (CADDR X))
47800 (QUOTE (OR (NOT (MODEL C1)) (NOT (MODEL C2)))))
47900 ((EQ (CAR X) (QUOTE DEFMODEL))
48000 (LIST (QUOTE OR)
48100 (LIST (QUOTE NOT) (LIST (CDR X) (QUOTE C1)))
48200 (LIST (QUOTE NOT) (LIST (CDR X) (QUOTE C2)))))
48300 ((EQ (CAR X) (QUOTE ANCESTRY)) (SETQ ANCESTRY T) (BUILTCH1 (CDR X)))
48400 ((ATOM (CAR X)) (CONS (BUILTCH1 (CAR X)) (BUILTCH1 (CDR X))))
48500 ((EQ (CAAR X) (QUOTE EQUALITY)) (SETQ PFLG NIL)
48600 (SETQ EQUAL (CADAR X))
48700 (SETQ PDEPTH (CADDAR X))
48800 (BUILTCH1 (CDR X)))
48900 (T (CONS (BUILTCH1 (CAR X)) (BUILTCH1 (CDR X))))))
49000 EXPR)
49100
49200 (DEFPROP CHOICE
49300 (LAMBDA(X)
49400 (PROG (Z Z1 Z2)
49500 (COND ((NOT (HERE X)) (RETURN NIL)) (ANCESTRY (SETQ Z (CHOICE1 X LLST))) (T (SETQ Z CLAUSES)))
49600 A (SETQ Z1 (CAR Z))
49700 (COND
49800 ((OR (NOT (HERE Z1))
49900 (AND PFLG (ALLPOS X) (ALLPOS Z1))
50000 (AND (ALLNEG Z1) (ALLNEG X))
50100 (AND STRATEGY (NOT (STRATEGY X Z1))))
50200 NIL)
50300 (T (SETQ Z2 (NCONC Z2 (LIST Z1)))))
50400 (SETQ Z (CDR Z))
50500 (COND ((OR (EQ Z X) (NULL Z)) (RETURN Z2)))
50600 (GO A)))
50700 EXPR)
50800
50900 (DEFPROP CHOICE1
51000 (LAMBDA (L LL) (COND ((ATOM (CDR (ANCESTOR L))) LL) (T (NCONC (CDR (TRAVERSE L)) LL))))
51100 EXPR)
51200
51300 (DEFPROP CLAUSES
51400 (LAMBDA (U) (PROG (DEBUG) (SETQ DEBUG T) (RETURN (CLAUSES1 U 1))))
51500 EXPR)
51600
51700 (DEFPROP CLAUSES2
51800 (LAMBDA (U) (CLAUSES1 U CNT))
51900 EXPR)
52000
52100 (DEFPROP CLAUSES1
52200 (LAMBDA(U N)
52300 (PROG NIL
52400 (COND ((NOT DEBUG) (RETURN NIL)))
52500 (COND ((NULL (CAR U)) (RETURN NIL)))
52600 CL1 (COND ((NULL U) (RETURN NIL)))
52700 (UP1A (CAR U) N)
52800 CL2 (SETQ U (CDR U))
52900 (SETQ N (ADD1 N))
53000 (GO CL1)))
53100 EXPR)
53200
53300 (DEFPROP CNF
53400 (LAMBDA(C1)
53500 (PROG (C)
53600 (SETQ C (PRECNF C1))
53700 (RETURN (CNF2 (COND ((EQ (CAR C) (QUOTE NOT)) (CNF1 (CADR C) NIL NIL NIL)) (T (CNF1 C NIL NIL T)))))))
53800 EXPR)
53900
54000 (DEFPROP CNF1
54100 (LAMBDA(C UNL EXL PF)
54200 (COND ((EQ (CAR C) (QUOTE NOT)) (CNF1 (CADR C) UNL EXL (COND (PF NIL) (T T))))
54300 ((MEMQ (CAR C) (QUOTE (AND OR)))
54400 (ANDOR (LIST (CAR C) (CNF1 (CADR C) UNL EXL PF) (CNF1 (CADDR C) UNL EXL PF)) UNL EXL PF))
54500 ((OR (AND (EQ (CAR C) (QUOTE FA)) PF) (AND (EQ (CAR C) (QUOTE TE)) (NOT PF)))
54600 (CNF1 (CADDR C) (APPEND (CADR C) UNL) EXL PF))
54700 ((OR (EQ (CAR C) (QUOTE FA)) (EQ (CAR C) (QUOTE TE)))
54800 (CNF1 (CADDR C) UNL (APPEND (GENSKOLEM (CADR C) UNL) EXL) PF))
54900 (PF (SUBSKOL C EXL))
55000 (T (CONS ESCAPE (SUBSKOL C EXL)))))
55100 EXPR)
55200
55300 (DEFPROP CNF2
55400 (LAMBDA(C)
55500 (COND ((EQ (CAR C) (QUOTE AND)) (APPEND (CNF2 (CADR C)) (CNF2 (CADDR C))))
55600 ((EQ (CAR C) (QUOTE OR)) (LIST (CNF3 C)))
55700 (T (LIST (LIST C)))))
55800 EXPR)
55900
56000 (DEFPROP CNF3
56100 (LAMBDA (C) (COND ((NOT (EQ (CAR C) (QUOTE OR))) (LIST C)) (T (APPEND (CNF3 (CADR C)) (CNF3 (CADDR C))))))
56200 EXPR)
56300
56400 (DEFPROP CNVT
56500 (LAMBDA(Z)
56600 (PROG (ZP ZN VARL VARNO)
56700 (SETQ VARNO 0)
56800 (COND
56900 ((EQ (LENGTH Z) 1)
57000 (RETURN (COND ((EQ (CAAR Z) ESCAPE) (LIST (QUOTE NOT) (CNVT2 (CDAR Z)))) (T (CNVT2 (CAR Z)))))))
57100 A1 (COND ((EQ (CAAR Z) ESCAPE) (GO AN1)))
57200 (SETQ ZP (CNVT2 (CAR Z)))
57300 AP1 (SETQ Z (CDR Z))
57400 (COND ((NULL Z) (GO AN2)) ((EQ (CAAR Z) ESCAPE) (GO AN1)))
57500 (SETQ ZP (LIST (QUOTE OR) (CNVT2 (CAR Z)) ZP))
57600 (GO AP1)
57700 AN1 (SETQ ZN (CNVT2 (CDAR Z)))
57800 AN1B (SETQ Z (CDR Z))
57900 AN1A (COND ((NULL Z) (GO AN2)))
58000 (SETQ ZN (LIST (QUOTE AND) (CNVT2 (CDAR Z)) ZN))
58100 (GO AN1B)
58200 AN2 (COND ((NULL ZP) (RETURN (LIST (QUOTE NOT) ZN)))
58300 ((NULL ZN) (RETURN ZP))
58400 (T (RETURN (LIST (QUOTE IMP) ZN ZP))))))
58500 EXPR)
58600
58700 (DEFPROP CNVT2
58800 (LAMBDA(X)
58900 (COND ((ATOM X) X)
59000 ((VAR (CAR X)) (CONS (CNVT3 (CAR X)) (CNVT2 (CDR X))))
59100 ((CONST (CAR X)) (CONS (CAR X) (CNVT2 (CDR X))))
59200 (T (CONS (CNVT2 (CAR X)) (CNVT2 (CDR X))))))
59300 EXPR)
59400
59500 (DEFPROP CNVT3
59600 (LAMBDA(X)
59700 (PROG (Z)
59800 (SETQ Z (ASSOC X VARL))
59900 (COND (Z (RETURN (CDR Z))))
60000 (SETQ VARL (CONS (CONS X (SETQ VARNO (ADD1 VARNO))) VARL))
60100 (RETURN VARNO)))
60200 EXPR)
60300
60400 (DEFPROP COPY
60500 (LAMBDA (X) (COND ((ATOM X) X) (T (CONS (COPY (CAR X)) (COPY (CDR X))))))
60600 EXPR)
60700
60800 (DEFPROP COPYDELETED
60900 (LAMBDA (X) (LIST (CONS (CONS NIL (CDAR X)) (CDR X))))
61000 EXPR)
61100
61200 (DEFPROP *CL
61300 (LAMBDA (C) (UPGETL1 C XYZ1 (CONS (CONS (QUOTE CLAUSES) XYZ1) NEWNAME)))
61400 EXPR)
61500
61600 (DEFPROP DEMOD
61700 (LAMBDA(X L)
61800 (PROG (S1 S2)
61900 (SETQ S1 (CDAR X))
62000 A (COND ((NEG (CAR S1)) (DEM (TCOPY (CDR (SETQ S2 (CDAR S1)))) 1 DDEPTH L))
62100 (T (DEM (TCOPY (CDR (SETQ S2 (CAR S1)))) 1 DDEPTH L)))
62200 (COND ((EQ (CAR S2) EQUAL) (ORDEREQUAL (CDR S2))))
62300 (SETQ S1 (CDR S1))
62400 (COND (S1 (GO A)))
62500 (RETURN X)
62575 ))
62600 EXPR)
62700
62800 (DEFPROP DEM
62900 (LAMBDA (T1 M N L) (COND ((OR (NULL T1) (EQ N M)) NIL) (T (PROG2 (DEM (PTRS T1) (ADD1 M) N L) (SUB* T1 L)))))
63000 EXPR)
63100
63200 (DEFPROP DEPTH
63300 (LAMBDA(Z)
63400 (PROG (Z1 Z2)
63500 (SETQ Z1 0)
63600 D1 (COND ((NEG (CAR Z)) (SETQ Z2 (CDDAR Z))) (T (SETQ Z2 (CDAR Z))))
63700 (SETQ Z1 (MAX Z1 (DEPTH1 Z2)))
63800 (SETQ Z (CDR Z))
63900 (COND (Z (GO D1)))
64000 (RETURN Z1)))
64100 EXPR)
64200
64300 (DEFPROP DEPTH
64400 (NIL . 10)
64500 VALUE)
64600
64700 (DEFPROP DEPTH1
64800 (LAMBDA(Z)
64900 (PROG (Z1)
65000 (SETQ Z1 0)
65100 D1 (COND ((OR (VAR (CAR Z)) (CONST (CAR Z))) (GO D2)))
65200 (SETQ Z1 (MAX Z1 (ADD1 (DEPTH1 (CDAR Z)))))
65300 D2 (SETQ Z (CDR Z))
65400 (COND (Z (GO D1)))
65500 (RETURN Z1)))
65600 EXPR)
65700
65800 (DEFPROP DEL
65900 (LAMBDA (C) (RPLACA (CAR C) NIL))
66000 EXPR)
66100
66200 (DEFPROP DOML
66300 (LAMBDA NIL (TERMS1 (COND ((NEG (CAR L)) (CDDAR L)) (T (CDAR L))) 100))
66400 EXPR)
66500
66600 (DEFPROP DOMC
66700 (LAMBDA NIL (CDR C))
66800 EXPR)
66900
67000 (DEFPROP DOWN
67100 (LAMBDA(N L)
67200 (PROG NIL
67300 (COND ((NOT (AND (NUMBERP N) (GREATERP N 0))) (RETURN NIL)))
67400 D1 (SETQ N (SUB1 N))
67500 (COND ((ZEROP N) (RETURN L)))
67600 (SETQ L (CDR L))
67700 (COND (L (GO D1)))
67800 (RETURN NIL)))
67900 EXPR)
68000
68100 (DEFPROP EDIT
68200 (LAMBDA(U Z)
68300 (PROG (RES1 U1 U4)
68400 ED4 (COND ((NULL Z) (RETURN RES1)))
68500 (SETQ U4 (CAR Z))
68600 (COND ((EDITSTRAT U4) (GO ED2)))
68700 (SETQ U1 SUBCLAUSES)
68800 ED1 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
68900 ED6 (SETQ U1 (CDR U1))
69000 (COND (U1 (GO ED1)))
69100 (SETQ U1 (CDR Z))
69200 (COND ((NULL U1) (GO ED5)))
69300 ED3 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
69400 ED7 (SETQ U1 (CDR U1))
69500 (COND (U1 (GO ED3)))
69600 ED5 (SETQ RES1 (CONS U4 RES1))
69700 ED2 (SETQ Z (CDR Z))
69800 (GO ED4)))
69900 EXPR)
70000
70100 (DEFPROP ERPRINT
70200 (LAMBDA (X) (COND (DEBUG (PRINT X))))
70300 EXPR)
70400
70500 (DEFPROP ERPRIN1
70600 (LAMBDA (X) (COND (DEBUG (PRIN1 X))))
70700 EXPR)
70800
70900 (DEFPROP EXPUNGE
71000 (LAMBDA (L) (PROG NIL A (COND ((NULL L) (RETURN NIL))) (DEL (CAR L)) (SETQ L (CDR L)) (GO A)))
71100 EXPR)
71200
71300 (DEFPROP FINI
71400 (LAMBDA(U R Z1 Z2 E)
71500 (PROG (Z)
71600 (COND (UFLG (SETQ R (UNITREDUCT R UNAXP UNAXN))))
71700 (COND ((NULL R) (RETURN 0)) ((NULL (CAR R)) (PROOF Z1 Z2) (ERR (QUOTE (QED)))))
71800 (SETQ COUNT (PLUS COUNT (LENGTH R)))
71900 (SETQ R (EDIT U R))
72000 (CLAUSES2 R)
72100 (COND ((NULL R) (RETURN 0)))
72200 (BAKSUB CLAUSES R)
72300 (BOOKEEP E R (CONS Z1 Z2))
72400 (SETQ Z (UNITPN R))
72500 (SETQ UNAXP (APPEND (CAR Z) UNAXP))
72600 (SETQ UNAXN (APPEND (CDR Z) UNAXN))
72700 (RETURN (LENGTH R))))
72800 EXPR)
72900
73000 (DEFPROP FIXNEG
73100 (LAMBDA (X) (COND ((EQ (CAR X) ESCAPE) (LIST (QUOTE NOT) (COPY (CDR X)))) (T (COPY X))))
73200 EXPR)
73300
73400 (DEFPROP FIXQFF
73500 (LAMBDA(C)
73600 (PROG (Z)
73700 (SETQ Z (FIXQFF1 C NIL NIL NIL))
73800 (COND ((NULL (CAR Z)) (RETURN C)) (T (RETURN (LIST (QUOTE FA) (CAR Z) C))))))
73900 EXPR)
74000
74100 (DEFPROP FIXQFF1
74200 (LAMBDA(C NEW FA TE)
74300 (PROG (Z)
74400 (COND ((NULL C) (RETURN (CONS NEW (CONS FA TE))))
74500 ((EQ (CAR C) (QUOTE FA)) (RETURN (FIXQFF1 (CADDR C) NEW (APPEND (CADR C) FA) TE)))
74600 ((EQ (CAR C) (QUOTE TE)) (RETURN (FIXQFF1 (CADDR C) NEW FA (APPEND (CADR C) TE))))
74700 ((EQ (CAR C) (QUOTE NOT)) (RETURN (FIXQFF1 (CADR C) NEW FA TE)))
74800 ((MEMQ (CAR C) (QUOTE (AND OR IMP EQUIV))) (SETQ Z (FIXQFF1 (CADR C) NEW FA TE))
74900 (RETURN
75000 (FIXQFF1 (CADDR C) (CAR Z) (CADR Z) (CDDR Z)))))
75100 (SETQ Z (GETVARS (COND ((NEG C) (CDDR C)) (T (CDR C)))))
75200 A (COND ((NULL Z) (RETURN (CONS NEW (CONS FA TE))))
75300 ((OR (MEMBER (CAR Z) NEW) (MEMBER (CAR Z) FA) (MEMBER (CAR Z) TE)) (GO B)))
75400 (SETQ NEW (CONS (CAR Z) NEW))
75500 B (SETQ Z (CDR Z))
75600 (GO A)))
75700 EXPR)
75800
75900 (DEFPROP GENSKOLEM
76000 (LAMBDA(VARL UNL)
76100 (PROG (Z)
76200 A (COND ((NULL VARL) (RETURN Z)))
76300 (SETQ Z (CONS (CONS (CAR VARL) (CONS (MKSYM) UNL)) Z))
76400 (SETQ VARL (CDR VARL))
76500 (GO A)))
76600 EXPR)
76700
76800 (DEFPROP GETNAME
76900 (LAMBDA(X L)
77000 (PROG (Z)
77100 (SETQ Z (ASSOC X L))
77200 (COND (Z (RETURN (CDR Z))))
77300 (PRINT X)
77400 (PRINC (QUOTE IS-AN-UNBOUND-NAME))
77500 (RETURN NIL)))
77600 EXPR)
77700
77800 (DEFPROP GETTERMS
77900 (LAMBDA NIL
78000 (PROG (Z Z1)
78100 (SCANSET)
78200 (START)
78300 (SETQ Z (ERRSET (<TM>) T))
78400 (SCANRESET)
78500 (COND ((OR (NULL Z) (NULL (CAR Z))) (RETURN NIL)))
78600 (SETQ XYZ (TOP))
78700 (COND ((NOT (EQ (READ) (QUOTE FOR))) (RETURN NIL)))
78800 (SCANSET)
78900 (START)
79000 (SETQ Z (ERRSET (<TM>) T))
79100 (SCANRESET)
79200 (COND ((OR (NULL Z) (NULL (CAR Z))) (RETURN NIL)))
79300 (SETQ XYZ1 (TOP))
79400 (COND ((NOT (EQ (READ) (QUOTE IN))) (RETURN NIL)))
79500 (RETURN (UPGETL E NAMELIST))))
79600 EXPR)
79700
79800 (DEFPROP GETVARS
79900 (LAMBDA(C)
80000 (PROG (Z)
80100 A (COND ((VAR (CAR C)) (SETQ Z (CONS (CAR C) Z)))
80200 ((CONST (CAR C)) NIL)
80300 (T (SETQ Z (APPEND (GETVARS (CDAR C)) Z))))
80400 (SETQ C (CDR C))
80500 (COND (C (GO A)))
80600 (RETURN Z)))
80700 EXPR)
80800
80900 (DEFPROP GOLIST
81000 (NIL (EO . UEO1)
81100 (DS . UDS1)
81200 (CH . UCH1)
81300 (SY . USY1)
81400 (CU . UCU1)
81500 (FL . UFL1)
81600 (DI . UDI1)
81700 (ST . UST1)
81800 (HA . UST1)
81900 (DE . UDE1)
82000 (IN . UIN1)
82100 (EV . UEV1)
82200 (QU . UQU1)
82300 (TR . UTR1)
82400 (UP . UUP1)
82500 (ME . UME1)
82600 (SI . USI1)
82700 (SE . USE1)
82800 (DO . UDO1)
82900 (CL . UCL1)
83000 (SU . USU1)
83100 (AN . UAN1)
83200 (TE . UTE1)
83300 (RE . URE1)
83400 (SA . USA1)
83500 (PA . UPA1)
83700 (ED . UED1)
83800 (US . UUS1)
83900 (PR . UPR1)
84000 (FU . UFL2)
84100 (FD . UFL3)
84200 (GO . UGO1)
84300 (EX . UEX1)
84400 (AB . UAB1)
84500 (HE . UHE1))
84600 VALUE)
84700
84800 (DEFPROP INCLAUSES
84900 (LAMBDA NIL
85000 (PROG (Z Z1 AXNO)
85100 (SETQ AXNO (QUOTE AXIOM))
85200 A (SCANSET)
85300 (START)
85400 (SETQ ZIN (ERRSET (<INPUT>) T))
85500 (SCANRESET)
85600 (COND ((OR (NULL ZIN) (NULL (CAR ZIN))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
85700 (SETQ ZIN (TOP))
85800 (COND ((EQ ZIN (QUOTE EMPTY)) (RETURN Z))
85900 ((ATOM ZIN) (PRIN1 ZIN) (SETQ AXNO (SETQ FNNAM ZIN)) (GO A))
86000 ((MEMQ (CAR ZIN) DECOP) (GO B)))
86100 (OUT >S< ZIN)
86200 (SETQ Z
86300 (APPEND Z
86400 (SETUP
86500 (CNF (COND ((EQ AXNO THEOREMNAME) (LIST (QUOTE NOT) (FIXQFF ZIN))) (T (FIXQFF ZIN)))))))
86600 (GO A)
86700 B (SETQ Z1 (CDR (ASSOC (CAR ZIN) DECTBL)))
86800 (COND ((EQ Z1 (QUOTE IVAR)) (MAKOVAR (SETQ IVAR (APPEND IVAR (CDR ZIN)))))
86900 ((EQ Z1 (QUOTE EQUAL)) (SETQ PFLG NIL) (SETQ EQUAL (CADR ZIN)))
87000 (T (SET Z1 (APPEND (CDR ZIN) (EVAL Z1)))))
87100 (OUT >INPUT< ZIN)
87200 (GO A)))
87300 EXPR)
87400
87500 (DEFPROP INITIAL
87600 (LAMBDA(L)
87700 (PROG (ST Z Z1 Z2)
87800 A (SETQ Z (CDR (ANCESTOR (CAR L))))
87900 (COND ((NOT (ATOM Z)) (PRINT (QUOTE LOSE-IN-INITIAL)) (ERR NIL))
88000 ((SETQ Z1 (ASSOC Z ST)) (RPLACD (LAST Z1) (LIST (CAR L))))
88100 (T (SETQ ST (CONS (CONS Z (LIST (CAR L))) ST))))
88200 (SETQ Z2 (CONS (CAR L) Z2))
88300 (SETQ L (CDR L))
88400 (COND (L (GO A)))
88500 (RETURN (REVERSE (CONS (CONS NIL NIL) (CONS (CONS (QUOTE %INITIAL) (REVERSE Z2)) ST))))))
88600 EXPR)
88700
88800 (DEFPROP INITIALAX
88900 (LAMBDA(L)
89000 (PROG (Z Z1 Z2 Z3 AXNO)
89100 (SETQ AXNO (CAR L))
89200 (SETQ L (CDR L))
89300 A (SETQ Z (CAR (SETUP (LIST (COPY (CDAR L))))))
89400 (SETQ Z1 (ANCESTOR (CAR L)))
89500 (COND ((ATOM (CAR Z1)) (SETQ Z1 (CDR Z1))))
89600 (SETQ Z2 (ANCESTOR Z))
89700 (RPLACA Z2 Z1)
89800 (RPLACD Z2 AXNO)
89900 (SETQ Z3 (CONS Z Z3))
90000 B0 (SETQ L (CDR L))
90100 (COND ((NULL L) (RETURN (REVERSE Z3))) ((ATOM (CAR L)) (SETQ AXNO (CAR L)) (GO B)))
90200 (GO A)))
90300 EXPR)
90400
90500 (DEFPROP INITIALAX1
90600 (LAMBDA(L1)
90700 (PROG (Z L2 L)
90800 (SETQ L L1)
90900 B1 (SETQ L2 L)
91000 A1 (COND ((EQ (CAR L) (CADR L2)) (RPLACD L2 (CDDR L2)) (GO A1)))
91100 (SETQ L2 (CDR L2))
91200 (COND (L2 (GO A1)))
91300 (SETQ L (CDR L))
91400 (COND (L (GO B1)))
91500 (SETQ L L1)
91600 B (SETQ Z (CDDAAR L))
91700 (COND ((NULL (CAAAR L)) (RPLACA (CAAR L) (LENGTH (CDAR L))))
91800 ((NUMBERP (CAAAR L)) NIL)
91900 (T (RPLACA (CAAR L) (CAAAAR L))))
92000 (COND ((ATOM (CDDR Z)) (GO A)))
92100 (RPLACD Z (CONS (CDR Z) (QUOTE DEDUCT)))
92200 A (SETQ L (CDR L))
92300 (COND (L (GO B)))
92400 (RETURN L1)))
92500 EXPR)
92600
92700 (DEFPROP MAKVAR
92800 (LAMBDA(X)
92900 (PROG (Z)
93000 (SETQ Z (ASSOC X VARTBL))
93100 (COND (Z (RETURN (CDR Z))))
93200 (SETQ VARTBL (CONS (CONS X (SETQ VARNO (ADD1 VARNO))) VARTBL))
93300 (RETURN VARNO)))
93400 EXPR)
93500
93600 (DEFPROP MAKOVAR
93700 (LAMBDA(X)
93800 (PROG (X1 *NOPOINT Z N M)
93900 (SETQ *NOPOINT T)
94000 (SETQ OUTVAR NIL)
94100 (SETQ N 1)
94200 (SETQ X1 X)
94300 D (SETQ OUTVAR (CONS (CONS N (CAR X1)) OUTVAR))
94400 (SETQ X1 (CDR X1))
94500 (SETQ N (ADD1 N))
94600 (COND (X1 (GO D)))
94700 B (SETQ Z (EXPLODE (CAR X)))
94800 (COND ((NUMBERP (CAR (LAST Z))) (GO A)))
94900 (SETQ M 1)
95000 C (SETQ OUTVAR (CONS (CONS N (READLIST (APPEND Z (LIST M)))) OUTVAR))
95100 (COND ((LESSP M 11) (SETQ N (ADD1 N)) (SETQ M (ADD1 M)) (GO C)))
95200 A (SETQ X (CDR X))
95300 (COND (X (SETQ N (ADD1 N)) (GO B)))
95400 (SETQ OUTVAR (REVERSE OUTVAR))
95500 (RETURN OUTVAR)))
95600 EXPR)
95700
95800 (DEFPROP MAPIT
95900 (LAMBDA(X XYZ N)
96000 (PROG (Z Z1 Z2)
96100 (SETQ Z (GETNAME X N))
96200 (COND ((NULL Z) (RETURN NIL)))
96300 A (SETQ ZIN (CAR Z))
96400 (SETQ Z2 (ERRSET (XYZ ZIN) T))
96500 (COND ((NULL Z2) (PRINT (QUOTE SCREWED-FIND)) (RETURN NIL))
96600 ((NULL (CAR Z2)) NIL)
96700 (T (SETQ Z1 (CONS (CAR Z) Z1))))
96800 (SETQ Z (CDR Z))
96900 (COND (Z (GO A)))
97000 (RETURN (REVERSE Z1))))
97100 EXPR)
97200
97300 (DEFPROP MATCHER
97400 (LAMBDA(L)
97500 (PROG (FLG Z Z1)
97600 (SETQ Z (EVAL (CADR L)))
97700 (SETQ Z1 (CAR L))
97800 (COND ((ATOM (CADR L))
97900 (COND ((MEMQ (CADR L) (QUOTE (T1 T2 T3 T4))) (SETQ FLG 4))
98000 ((MEMQ (CADR L) (QUOTE (L1 L2 L3 L4))) (SETQ FLG 3))
98100 ((MEMQ (CADR L) (QUOTE (C))) (SETQ FLG 2) (SETQ Z (CDR Z)))
98200 (T (ERR NIL))))
98300 ((EQ (CAADR L) (QUOTE TREE)) (SETQ FLG 1))
98400 (T (ERR NIL)))
98500 (COND ((ATOM Z1) (RETURN (MATCH1 Z1 Z FLG)))
98600 ((EQ (CAR Z1) (QUOTE AND)) (GO MAA1))
98700 ((EQ (CAR Z1) (QUOTE OR)) (GO MAO1))
98800 (T (RETURN (MATCH1 Z1 Z FLG))))
98900 MAA1 (SETQ Z1 (CDR Z1))
99000 MAAND
99100 (COND ((NULL Z1) (RETURN T)) ((MATCH1 (CAR Z1) Z FLG) (GO MAA1)) (T (RETURN NIL)))
99200 MAO1 (SETQ Z1 (CDR Z1))
99300 MAOR (COND ((NULL Z1) (RETURN NIL)) ((MATCH1 (CAR Z1) Z FLG) (RETURN T)))
99400 (GO MAO1)))
99500 FEXPR)
99600
99700 (DEFPROP MATCH1
99800 (LAMBDA(X Y FL)
99900 (COND ((ATOM X)
00100 (COND ((EQ X (QUOTE %NG)) (COND ((ISLIT FL) (NEG Y)) ((ISCL FL) (MATCHPN Y T)) (T (ERR NIL))))
00200 ((EQ X (QUOTE %PL)) (COND ((ISLIT FL) (NOT (NEG Y))) ((ISCL FL) (MATCHPN Y NIL)) (T (ERR NIL))))
00300 ((NUMBERP X) (COND ((ISCLS FL) (MATCHTR X Y)) (T (MATMLT X Y FL))))
00400 ((AND (MEMQ X (QUOTE (C1 C2))) (ISCLS FL)) (MEMQ (EVAL X) Y))
00500 (T (ERR NIL))))
00600 ((NUMBERP (CAR X)) (COND ((ISCLS FL) (MATCHTR (CAR X) Y)) (T (MATMLT (CAR X) Y FL))))
00700 ((EQ (LENGTH X) 1) (MATMLT (CAR X) Y FL))
00800 ((ISCLS FL) (COND ((EQ (CAR X) (QUOTE CL)) (MATCHTR (CADR X) Y)) (T NIL)))
00900 (T (MATMLT* X Y FL))))
01000 EXPR)
01100
01200 (DEFPROP MATCHTR
01300 (LAMBDA (N TR) (MEMQ (CAR (DOWN N CLAUSES)) TR))
01400 EXPR)
01500
01600 (DEFPROP MATCHPN
01700 (LAMBDA(X FL)
01800 (PROG (Z)
01900 A (SETQ Z (NEG (CAR X)))
02000 (COND ((AND Z FL) (RETURN T)) ((AND (NOT Z) (NOT FL)) (RETURN T)))
02100 (SETQ X (CDR X))
02200 (COND (X (GO A)))
02300 (RETURN NIL)))
02400 EXPR)
02500
02600 (DEFPROP MATMLT
02700 (LAMBDA(X Y FL)
02800 (PROG NIL
02900 (COND ((AND (ISTRM FL) (NOT (ASSOC X TBL))) (ERR NIL))
03000 ((ISTRM FL) (RETURN (OCR X Y)))
03100 ((ISLIT FL) (RETURN (COND ((NEG Y) (OCR X (CDR Y))) (T (OCR X Y))))))
03200 A (COND ((COND ((NEG (CAR Y)) (OCR X (CDAR Y))) (T (OCR X (CAR Y)))) (RETURN T)))
03300 (SETQ Y (CDR Y))
03400 (COND (Y (GO A)))
03500 (RETURN NIL)))
03600 EXPR)
03700
03800 (DEFPROP MATMLT*
03900 (LAMBDA(X Y FL)
04000 (PROG (Z)
04100 (COND ((AND (ISTRM FL) (NOT (ASSOC (CAR X) TBL))) (ERR NIL))
04200 ((EQ (CAR X) (QUOTE %NG)) (SETQ X (CDR X)) (GO M1))
04300 ((NOT (ISCL FL)) (SETQ Y (LIST Y))))
04400 D (SETQ X (VARIT (LIST X)))
04500 B (SETQ Z (TERMS1 (LIST (COND ((NEG (CAR Y)) (CDAR Y)) (T (CAR Y)))) 64))
04600 A (COND ((UNI X (CAR Z) NIL) (RETURN T)))
04700 (SETQ Z (CDR Z))
04800 (COND (Z (GO A)))
04900 (SETQ Y (CDR Y))
05000 (COND (Y (GO B)))
05100 (RETURN NIL)
05200 M1 (COND ((NEG (CAR Y)) (GO M2)))
05300 M3 (SETQ Y (CDR Y))
05400 (COND (Y (GO M1)))
05500 (RETURN NIL)
05600 M2 (COND ((EQ (LENGTH X) 1) (COND ((EQ (CADAR Y) (CAR X)) (RETURN T)) (T (GO M3)))) (T (GO D)))))
05700 EXPR)
05800
05900 (DEFPROP MAX
06000 (LAMBDA (X Y) (COND ((GREATERP X Y) X) (T Y)))
06100 EXPR)
06200
06300 (DEFPROP MEMC
06400 (LAMBDA(C L)
06500 (PROG NIL
06600 (COND ((NULL L) (RETURN NIL)) ((POS C) (GO A)))
06700 B (COND ((POS (CAR L)) (RETURN NIL)) ((EQUAL C (CAR L)) (RETURN T)))
06800 (SETQ L (CDR L))
06900 (COND (L (GO B)))
07000 (RETURN NIL)
07100 A (COND ((POS (CAR L)) (RETURN (MEMBER C L))))
07200 (SETQ L (CDR L))
07300 (COND (L (GO A)))
07400 (RETURN NIL)))
07500 EXPR)
07600
07700 (DEFPROP MIN1
07800 (LAMBDA(L)
07900 (PROG (Z Z1)
08000 (SETQ Z (CAR L))
08100 M1 (SETQ Z1 (CDR L))
08200 (COND ((NULL Z1)
08300 (COND ((NUMBERP (CAR Z)) (RETURN NIL)) (T (SETQ Z1 (COPY Z)) (RPLACA Z 0) (RETURN Z1))))
08400 ((NUMBERP (CAAR Z1)) (GO M2))
08500 ((OR (NUMBERP (CAR Z)) (ORDER Z (CAR Z1))) (SETQ Z (CAR Z1))))
08600 M2 (SETQ L (CDR L))
08700 (GO M1)))
08800 EXPR)
08900
09000 (DEFPROP MINIMIZE
09100 (LAMBDA(Z3)
09200 (PROG (Z1 Z2 Z4)
09300 (SETQ Z2 (LIST (CAR Z3)))
09400 ED2 (SETQ Z3 (CDR Z3))
09500 (COND ((NULL Z3) (RETURN (REVERSE Z2))))
09600 (SETQ Z4 (CAR Z3))
09700 (SETQ Z1 Z2)
09800 ED1 (COND ((SUBSUME (CAR Z1) Z4) (GO ED2)))
09900 (SETQ Z1 (CDR Z1))
10000 (COND (Z1 (GO ED1)))
10100 (SETQ Z1 (CDR Z3))
10200 ED4 (COND ((NULL Z1) (GO ED5)) ((SUBSUME (CAR Z1) Z4) (GO ED2)))
10300 (SETQ Z1 (CDR Z1))
10400 (GO ED4)
10500 ED5 (SETQ Z2 (CONS Z4 Z2))
10600 (GO ED2)))
10700 EXPR)
10800
10900 (DEFPROP MIN
11000 (LAMBDA (X Y) (COND ((LESSP X Y) X) (T Y)))
11100 EXPR)
11200
11300 (DEFPROP MKSYM
11400 (LAMBDA NIL
11500 (PROG NIL
11600 (SETQ FNLIST (CONS (READLIST (APPEND (EXPLODE FNNAM) (EXPLODE (SETQ FNNO (ADD1 FNNO))))) FNLIST))
11700 (SETQ PREFN (CONS (CAR FNLIST) PREFN))
11800 (RETURN (CAR FNLIST))))
11900 EXPR)
12000
12100 (DEFPROP MODEL
12200 (LAMBDA(C)
12300 (PROG (Z)
12400 (SETQ Z (CDR C))
12500 M1 (COND ((NEG (CAR Z)) (GO M3)) ((MEMBER (CAAR Z) PMODEL) (SETQ SAT C) (RETURN T)))
12600 M2 (SETQ Z (CDR Z))
12700 (COND (Z (GO M1)))
12800 (RETURN NIL)
12900 M3 (COND ((MEMBER (CADAR Z) NMODEL) (SETQ SAT C) (RETURN T)))
13000 (GO M2)))
13100 EXPR)
13200
13300 (DEFPROP NCONC1
13400 (LAMBDA (A B) (COND ((NULL A) B) ((NULL B) A) (T (RPLACD A B))))
13500 EXPR)
13600
13700 (DEFPROP NEGATE
13800 (LAMBDA(Z)
13900 (PROG (BDY)
14000 (COND ((EQ (LENGTH Z) 1) (SETQ BDY (FIXNEG (CAR Z))) (GO D)))
14100 (SETQ BDY (LIST (QUOTE OR) (FIXNEG (CADR Z)) (FIXNEG (CAR Z))))
14200 (SETQ Z (CDDR Z))
14300 C (COND ((NULL Z) (GO D)))
14400 (SETQ BDY (LIST (QUOTE OR) (FIXNEG (CAR Z)) BDY))
14500 (SETQ Z (CDR Z))
14600 (GO C)
14700 D (RETURN (SET3 (SETUP (CNF (LIST (QUOTE NOT) (FIXQFF BDY))))))))
14800 EXPR)
14900
15000 (DEFPROP NEGSGN
15100 (NIL . ¬)
15200 VALUE)
15300
15400 (DEFPROP NOSYM
15500 (LAMBDA (L) (COND ((NULL L) 0) ((ATOM L) 1) (T (MAX (ADD1 (NOSYM (CAR L))) (NOSYM (CDR L))))))
15600 EXPR)
15700
15800 (DEFPROP OCR
15900 (LAMBDA (X Y) (OCR1 X (LIST Y)))
16000 EXPR)
16100
16200 (DEFPROP OCR1
16300 (LAMBDA(X Y)
16400 (COND ((NULL Y) NIL)
16500 ((VAR (CAR Y)) (OCR1 X (CDR Y)))
16600 ((CONST (CAR Y)) (COND ((EQ (CAAR Y) X) T) (T (OCR1 X (CDR Y)))))
16700 ((EQ X (CAAR Y)) T)
16800 ((OCR1 X (CDAR Y)) T)
16900 (T (OCR1 X (CDR Y)))))
17000 EXPR)
17100
17200 (DEFPROP ONEGSGN
17300 (NIL . ¬)
17400 VALUE)
17500
17600 (DEFPROP *NOPOINT
17700 (NIL . T)
17800 VALUE)
17900
18000 (DEFPROP OCCUR
18100 (LAMBDA(X Z)
18200 (PROG (Z1)
18300 OC1 (SETQ Z1 (CAR Z))
18400 (COND ((VAR Z1) (COND ((EQ X Z1) (RETURN T)) (T (GO OC2))))
18500 ((CONST Z1) (GO OC2))
18600 ((OCCUR X (CDR Z1)) (RETURN T)))
18700 OC2 (SETQ Z (CDR Z))
18800 (COND (Z (GO OC1)))
18900 (RETURN NIL)))
19000 EXPR)
19100
19200 (DEFPROP ORDER
19300 (LAMBDA(X Y)
19400 (COND ((POS X) (COND ((POS Y) (ORDERP (CAR X) (CAR Y))) (T T)))
19500 ((NEG X) (COND ((NEG Y) (ORDERP (CADR X) (CADR Y))) (T NIL)))))
19600 EXPR)
19700
19800 (DEFPROP ORDEREQUAL
19900 (LAMBDA(S)
20000 (PROG NIL
20100 (COND ((VAR (CAR S))
20200 (COND ((VAR (CADR S)) (COND ((GREATERP (CADR S) (CAR S)) (GO A)) (T (RETURN NIL)))) (T (GO A))))
20300 ((CONST (CAR S))
20400 (COND ((VAR (CADR S)) (RETURN NIL))
20500 ((CONST (CADR S)) (COND ((ORDERP (CAAR S) (CAADR S)) (GO A)) (T (RETURN NIL))))
20600 (T (GO A))))
20700 ((OR (VAR (CADR S)) (CONST (CADR S))) (RETURN NIL))
20800 ((MAXDEPTH1(CDAR S)(DEPTH1(CDADR S)))(RETURN NIL)))
20900 A (PROG (S1) (SETQ S1 (CADR S)) (RPLACA (CDR S) (CAR S)) (RPLACA S S1))))
21000 EXPR)
21100
21110 (DE ORDEREQUAL1(X)(PROG(S1 S2)
21120 (SETQ S1(CDAR X))B(SETQ S2(COND((NEG(CAR S1))(CDAR S1))(T(CAR S1))))
21130 (COND((EQ(CAR S2 )EQUAL)(ORDEREQUAL (CDR S2))))
21140 (SETQ S1(CDR S1))(COND(S1(GO B)))(RETURN X)))
21150
21200 (DEFPROP PARMOD
21300 (LAMBDA(C D)
21400 (COND ((ALLNEG C) (PARMOD1 D C)) ((ALLNEG D) (PARMOD1 C D)) (T (NCONC (PARMOD1 C D) (PARMOD1 D C)))))
21500 EXPR)
21600
21700 (DEFPROP PARMOD1
21800 (LAMBDA(C D)
21900 (PROG (PF YC YD Z Z1 Z2 X Y Y1 Y2 PAR TS)
22000 (SETQ YC (CDR C))
22100 PAR1 (SETQ YD (CDR D))
22200 (SETQ X (CAR YC))
22300 (COND ((NEG X) (RETURN PAR))
22400 ((ORDERP (CAR X) EQUAL) (GO PAR2))
22500 ((NOT (EQ (CAR X) EQUAL)) (RETURN PAR)))
22600 PAR3 PAR3A
22700 (COND ((NEG (CAR YD)) (SETQ Z2 (CDAR YD))) (T (SETQ Z2 (CAR YD))))
22800 (SETQ Y1 (CDDR X))
22900 (SETQ Y2 (CADR X))
23000 PAR3B
23100 (COND ((VAR (CAR Y1)) (GO PAR7A)))
23200 (SETQ Z (TERMS (CAAR Y1) (CDR Z2) PDEPTH))
23300 (COND ((NULL Z) (GO PAR7A)))
23400 PAR5 (SETQ Z1 Z)
23500 PAR4 (COND
23600 ((CONST (CAR Y1))
23700 (COND ((OR (VAR (CAAR Z1)) (NOT (EQ (CAAR Y1) (CAAAR Z1)))) (GO PAR7))
23800 (T (SETQ TS (COPY Y2)) (GO PAR9))))
23900 ((OR (VAR (CAAR Z1)) (NOT (EQ (CAAR Y1) (CAAAR Z1)))) (GO PAR7)))
24000 (SETQ Y (UNIFY (CDAR Y1) (CDAAR Z1)))
24100 (COND (Y (SETQ Y (CDR Y)) (GO PAR6)))
24200 PAR7 (SETQ Z1 (CDR Z1))
24300 (COND (Z1 (GO PAR4)))
24400 PAR7A
24500 (COND ((NULL PF) (SETQ PF T) (SETQ Y1 (LIST Y2)) (SETQ Y2 (CADDR X)) (GO PAR3B)))
24600 PAR7B
24700 (SETQ YD (CDR YD))
24800 (COND (YD (GO PAR3A)))
24900 PAR2 (SETQ YC (CDR YC))
25000 (COND (YC (GO PAR1)))
25100 (RETURN PAR)
25200 PAR6 (SETQ TS (CADR (SUBS3T* Y (LIST NIL Y2))))
25300 PAR9 (SETQ PARRES (SUBS3TA Y Z2 (CAR Z1) TS))
25400 (COND ((NEG (CAR YD)) (SETQ PARRES (CONS ESCAPE PARRES))))
25500 (SETQ Y (UNION Y C D X (CAR YD)))
25600 (COND ((NULL Y) (GO PAR7)))
25700 (SETQ PAR (CONS (SET2 (CAR (COND (DLIST (DEMOD Y DLIST))(EQUAL(ORDEREQUAL1 Y)) (T Y))) TBL) PAR))
25800 (GO PAR7)))
25900 EXPR)
26000
26100 (DEFPROP POTZ
26200 (LAMBDA(X)
26300 (PROG (Z Z1)
26400 (SETQ Z (POTZ1 X))
26500 (COND ((SETQ Z1 (PMEMQ Z POTZTBL)) (RETURN Z1)))
26600 (SETQ POTZTBL (CONS Z POTZTBL))
26700 (RETURN Z)))
26800 EXPR)
26900
27000 (DEFPROP PRECNF
27100 (LAMBDA(X)
27200 (COND ((EQ (CAR X) (QUOTE NOT)) (LIST (QUOTE NOT) (PRECNF (CADR X))))
27300 ((MEMQ (CAR X) (QUOTE (AND OR))) (LIST (CAR X) (PRECNF (CADR X)) (PRECNF (CADDR X))))
27400 ((MEMQ (CAR X) (QUOTE (FA TE))) (LIST (CAR X) (CADR X) (PRECNF (CADDR X))))
27500 ((EQ (CAR X) (QUOTE IMP)) (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X))))
27600 ((EQ (CAR X) (QUOTE EQUIV))
27700 (LIST (QUOTE AND)
27800 (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X)))
27900 (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (COPY (CADDR X)))) (PRECNF (COPY (CADR X))))))
28000 (T X)))
28100 EXPR)
28200
28300 (DEFPROP PROOF1
28400 (LAMBDA(L)
28500 (PROG (Q X Y Z P P1)
28600 (PRINC (QUOTE / ))
28700 (PRINC (QUOTE / ))
28800 (PRFPRINT (CDR L))
28900 (SETQ P (ANCESTOR L))
29000 (COND ((ATOM (CDR P)) (GO P3)))
29100 (SETQ P1 (CDR P))
29200 (SETQ P (CAR P))
29300 (PRINC (QUOTE / ))
29400 (PRINC 1)
29500 (PRINC (QUOTE / ))
29600 (PRINC 2)
29700 (SETQ X 1)
29800 (SETQ Y 2)
29900 (SETQ Q (LIST (CONS X P) (CONS Y P1)))
30000 P1 (SETQ Z (ANCESTOR (CDAR Q)))
30100 (COND ((ATOM (CDR Z)) (PRINT (CAAR Q)) (PRFPRINT (CDDAR Q)) (PRIN1 (CDR Z)) (GO P2)))
30200 (SETQ X (ADD1 Y))
30300 (SETQ Y (ADD1 X))
30400 (PRINT (CAAR Q))
30500 (PRFPRINT (CDDAR Q))
30600 (PRINC X)
30700 (PRINC (QUOTE / ))
30800 (PRINC Y)
30900 (SETQ Q (NCONC Q (LIST (CONS X (CAR Z)) (CONS Y (CDR Z)))))
31000 P2 (SETQ Q (CDR Q))
31100 (COND ((NULL Q) (RETURN NIL)))
31200 (GO P1)
31300 P3 (PRIN1 (CDR P))
31400 (RETURN (TERPRI))))
31500 EXPR)
31600
31700 (DEFPROP PROVE
31800 (LAMBDA (L) (PROG (AUTO) (SETQ AUTO T) (EVAL (CONS (QUOTE TRY1) L))))
31900 FEXPR)
32000
32100 (DEFPROP PRPAR
32200 (LAMBDA(L)
32300 (PROG NIL
32400 (CLAUSES CLAUSES)
32500 (TERPRI)
32600 P1 (PROOF1 (CAR L))
32700 (TERPRI)
32800 (TERPRI)
32900 (SETQ L (CDR L))
33000 (COND (L (GO P1)))
33100 (RETURN NIL)))
33200 EXPR)
33300
33400 (DEFPROP PRFPRINT
33500 (LAMBDA(X)
33600 (PROG NIL
33700 (SETQ &&Z (FUNFLAT (LIST (LIST (OUTTST (CNVT X) (FUNCTION >S<))))))
33800 (SETQ LAST NIL)
33900 (FPRINT &&Z 0)))
34000 EXPR)
34100
34200 (DEFPROP PRFPR1
34300 (LAMBDA(L)
34400 (PROG (Z)
34500 (COND ((NEG L) (PRINC ONEGSGN) (SETQ L (CDR L))))
34600 (PRINC (CAR L))
34700 (SETQ L (CDR L))
34800 (PRINC (QUOTE /())
34900 P1 (COND ((VAR (CAR L))
35000 (COND ((MINUSP (CAR L)) (PRINC (QUOTE Z)) (PRINC (MINUS (CAR L))))
35100 (T (PRINC (QUOTE X))
35200 (COND ((SETQ Z (ASSOC (CAR L) VARL)) (PRINC (CDR Z)))
35300 (T (SETQ VARL (CONS (CONS (CAR L) (SETQ ONO (ADD1 ONO))) VARL)) (PRINC ONO))))))
35400 ((CONST (CAR L)) (PRINC (CAAR L)))
35500 (T (PRFPR1 (CAR L))))
35600 P2 (SETQ L (CDR L))
35700 (COND ((NULL L) (PRINC (QUOTE /))) (RETURN NIL)))
35800 (PRINC (QUOTE /,))
35900 (GO P1)))
36000 EXPR)
36100
36200 (DEFPROP PROOF
36300 (LAMBDA(L R)
36400 (PROG (Q Q1 X Z)
36500 (SETQ LHP L)
36600 (SETQ RHP R)
36700 (RPLACA (MKWRD L) 1)
36800 (RPLACA (MKWRD R) 2)
36900 (SETQ X 2)
37000 (SETQ Q (LIST L R))
37100 (SETQ Q1 Q)
37200 P1 (SETQ Z (ANCESTOR (CAR Q)))
37300 (COND ((ATOM (CDR Z)) (COND ((NOT (ATOM (CAR Z))) (SETQ Z (CAR Z))) (T (GO P2)))))
37400 (RPLACA (MKWRD (CAR Z)) (SETQ X (ADD1 X)))
37500 (RPLACA (MKWRD (CDR Z)) (SETQ X (ADD1 X)))
37600 (NCONC Q (LIST (CAR Z) (CDR Z)))
37700 P2 (SETQ Q (CDR Q))
37800 (COND (Q (GO P1)))
37900 (PRINT (QUOTE NIL))
38000 (PRINC (CAR (MKWRD (CAR Q1))))
38100 (PRINC (QUOTE / ))
38200 (PRINC (CAR (MKWRD (CADR Q1))))
38300 (SETQ X 1)
38400 A (COND
38500 ((EQ (CAR (MKWRD (CAR Q1))) X) (PRINT X)
38600 (PRFPRINT (CDAR Q1))
38700 (COND
38800 ((ATOM (CAR (ANCESTOR (CAR Q1)))) (PRIN1 (CAR (ANCESTOR (CAR Q1)))))
38900 ((ATOM (CDR (ANCESTOR (CAR Q1))))
39000 (PRINC (CAR (MKWRD (CAAR (ANCESTOR (CAR Q1))))))
39100 (PRINC (QUOTE / ))
39200 (PRINC (CAR (MKWRD (CDAR (ANCESTOR (CAR Q1)))))))
39300 (T (PRINC (CAR (MKWRD (CAR (ANCESTOR (CAR Q1))))))
39400 (PRINC (QUOTE / ))
39500 (PRINC (CAR (MKWRD (CDR (ANCESTOR (CAR Q1))))))))))
39600 (SETQ Q1 (CDR Q1))
39700 (SETQ X (ADD1 X))
39800 (COND (Q1 (GO A)))))
39900 EXPR)
40000
40100 (DEFPROP PTRS
40200 (LAMBDA(X)
40300 (PROG (Z)
40400 A (COND ((VAR (CAAR X)) NIL) ((CONST (CAAR X)) NIL) (T (SETQ Z (APPEND (TCOPY (CDAAR X)) Z))))
40500 (SETQ X (CDR X))
40600 (COND (X (GO A)))
40700 (RETURN Z)))
40800 EXPR)
40900
41000 (DEFPROP PUNIFY
41100 (LAMBDA(X Y)
41200 (PROG (LC Z1 Z2 Z3 Z4 Z6 Z7)
41300 (SETQ LC (LIST NIL))
41400 U3 (SETQ Z1 (CAR X))
41500 (SETQ Z2 (CAR Y))
41600 (COND ((VAR Z1) (SETQ Z3 (SEARCH Z1 (CDR LC)))) (T (SETQ Z3 Z1)))
41700 (COND ((VAR Z2) (SETQ Z4 (SEARCH Z2 (CDR LC)))) (T (SETQ Z4 Z2)))
41800 (COND ((VAR Z3)
41900 (COND ((VAR Z4) (GO UN1))
42000 ((CONST Z4) (GO UN3))
42100 (T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z3 (COPY Z4)))) (GO UN2))
42200 ((NOT (VAR Z2)) (SETQ Z4 (SUBS3T* (CDR LC) Z4))))
42300 (COND ((OCCUR Z3 (CDR Z4)) (RETURN NIL)) (T (GO UN3))))))
42400 ((VAR Z4) (RETURN NIL))
42500 ((AND (CONST Z3) (CONST Z4)) (COND ((NOT (EQ (CAR Z3) (CAR Z4))) (RETURN NIL)) (T (GO UN2))))
42600 ((EQ (CAR Z3) (CAR Z4)) (SETQ Z6 (CDR (SUBS3T* (CDR LC) Z3)))
42700 (SETQ Z7 (CDR (SUBS3T* (CDR LC) Z4)))
42800 (SETQ X (APPEND Z6 (CDR X)))
42900 (SETQ Y (APPEND Z7 (CDR Y)))
43000 (GO U3))
43100 (T (RETURN NIL)))
43200 UN1 (SUBS2T Z3 Z4 LC)
43300 UN2 (SETQ X (CDR X))
43400 (COND (X (SETQ Y (CDR Y)) (GO U3)))
43500 (RETURN LC)
43600 UN3 (SUBS2T Z4 Z3 LC)
43700 (GO UN2)))
43800 EXPR)
43900
44000 (DEFPROP QUERY
44100 (LAMBDA NIL
44200 (PROG NIL
44300 (PRINT (QUOTE CHOICE-STRATEGY-IS:))
44400 (OUTIT SAVESTR)
44500 (PRINT (QUOTE EDIT-STRATEGY-IS:))
44600 (OUTIT SAVEED)
44700 (PRINT (QUOTE ELAPSED-TIME))
44800 (PRINC (QUOTE =))
44900 (PRINC (TIMEIT))
45000 (RETURN (TERPRI))))
45100 EXPR)
45200
45300 (DEFPROP REAL-LNGTH
45400 (LAMBDA(L)
45500 (PROG (N)
45600 (SETQ N 0)
45700 A (COND ((NULL (CDR L)) (RETURN N)) ((HERE (CAR L)) (SETQ N (ADD1 N))))
45800 (SETQ L (CDR L))
45900 (GO A)))
46000 EXPR)
46100
46200 (DEFPROP REDUCER
46300 (LAMBDA(C L)
46400 (PROG (Z Z1 Z2 Z3 C1)
46500 (SETQ Z (CDAR C))
46600 (SETQ Z2 (CDAAR C))
46700 (SETQ C1 C)
46800 (SETQ Z3 (SETQ Z1 (CONS NIL (CAR Z2))))
46900 A (COND ((EQ L (CDR C1)) (GO B)))
47000 (SETQ C1 (CDR C1))
47100 (SETQ Z1 (CDR Z1))
47200 (GO A)
47300 B (RPLACD C1 (CDDR C1))
47400 (COND ((EQ (CAR Z) L) (RPLACA Z (CDR L))))
47500 (COND ((EQ (CDR Z2) (CDR Z1)) (RPLACD Z2 (CDDR Z2))))
47600 (RPLACD Z1 (CDDR Z1))
47700 (RPLACA Z2 (CDR Z3))
47800 (RPLACA (CAAR C) (SUB1 (CAAAR C)))
47900 (RETURN C)))
48000 EXPR)
48100
48200 (DEFPROP RESOLVE
48300 (LAMBDA(C D)
48400 (COND ((OR (ALLNEG D) (ALLPOS C)) (RESOLVE1 C D))
48500 ((OR (ALLPOS D) (ALLNEG C)) (RESOLVE1 D C))
48600 (T (NCONC (RESOLVE1 C D) (RESOLVE1 D C)))))
48700 EXPR)
48800
48900 (DEFPROP RESOLVE1
49000 (LAMBDA(C D)
49100 (PROG (CB DB DB1 YC YD YD1 Z X Y RES)
49200 (COND ((AND COND (EVAL COND)) (ERR (CDR LCL))))
49300 (SETQ YC (CDR C))
49400 (SETQ CB (POSBIT C))
49500 (SETQ YD1 (NEGL D))
49600 (SETQ DB1 (NEGBIT D))
49700 (SETQ DB DB1)
49800 (SETQ YD YD1)
49900 RES1 (SETQ X (CAR YC))
50000 (COND ((NEG X) (RETURN RES)))
50100 (SETQ Y (CAR YD))
50200 (COND ((ORDERP (CAR X) (CADR Y)) (GO RES3)) ((NOT (EQ (CAR X) (CADR Y))) (GO RES4)))
50300 (SETQ YD1 YD)
50400 (SETQ DB1 DB)
50500 (GO RES2A)
50600 RES2 (SETQ Y (CAR YD))
50700 (COND ((NOT (EQ (CAR X) (CADR Y))) (GO RES3A)))
50800 RES2A
50900 (COND ((NOT (UNIFAB (CAR CB) (CAR DB))) (GO RES2B)))
51000 (SETQ Z (UNIFY (CDR X) (CDDR Y)))
51100 (COND ((NULL Z) (GO RES2B)))
51200 (SETQ PARRES NIL)
51300 (SETQ Z (UNION (CDR Z) C D X Y))
51400 (COND ((NULL Z) (GO RES2B)) ((NULL (CAR Z)) (RETURN Z)))
51500 (SETQ RES (CONS (SET2 (CAR (COND (DLIST (DEMOD Z DLIST))(EQUAL(ORDEREQUAL1 Z)) (T Z))) TBL) RES))
51600 RES2B
51700 (SETQ YD (CDR YD))
51800 (COND (YD (SETQ DB (CDR DB)) (GO RES2)))
51900 RES3A
52000 (SETQ DB DB1)
52100 (SETQ YD YD1)
52200 RES3 (SETQ YC (CDR YC))
52300 (COND (YC (SETQ CB (CDR CB)) (GO RES1)))
52400 (RETURN RES)
52500 RES4 (SETQ YD (CDR YD))
52600 (COND (YD (SETQ DB (CDR DB)) (GO RES1)))
52700 (GO RES3A)))
52800 EXPR)
52900
53000 (DEFPROP RESUNITP
53100 (LAMBDA(P TM L)
53200 (PROG (Z)
53300 A (SETQ Z (CDADAR L))
53400 (COND ((EQ (CAR Z) P) (GO C)))
53500 B (SETQ L (CDR L))
53600 (COND (L (GO A)))
53700 (RETURN NIL)
53800 C (COND ((UNIFY (CDR Z) TM) (RETURN (LIST NIL))))
53900 (GO B)))
54000 EXPR)
54100
54200 (DEFPROP RESUNITN
54300 (LAMBDA(P TM L)
54400 (PROG (Z)
54500 A (SETQ Z (CADAR L))
54600 (COND ((EQ (CAR Z) P) (GO C)))
54700 B (SETQ L (CDR L))
54800 (COND (L (GO A)))
54900 (RETURN NIL)
55000 C (COND ((UNIFY (CDR Z) TM) (RETURN (LIST NIL))))
55100 (GO B)))
55200 EXPR)
55300
55400 (DEFPROP RESET
55500 (LAMBDA(L)
55600 (PROG (Z) R1 (SETQ Z (EVAL (CONS (QUOTE RESET1) (CAR L)))) (SETQ L (CDR L)) (COND (L (GO R1))) (RETURN Z)))
55700 FEXPR)
55800
56200
56300 (DEFPROP RESET1
56400 (LAMBDA(L)
56500 (PROG (X Z2 Z3 ZZ XX Z Z1 F1)
56600 (SETQ Z STATEVECTOR)
56700 A (COND
56800 ((EQ (CAR L) (CAR Z)) (SETQ F1 T)
56900 (COND ((EQ (CAR L) (QUOTE STRATEGY)) (GO R1))
57000 (T (SET (CAR Z) (EVAL (CADR L)))))))
57100 R2 (SETQ Z1 (CONS (EVAL (CAR Z)) Z1))
57200 (SETQ Z (CDR Z))
57300 (COND (Z (GO A)))
57400 (COND (F1 (RETURN (REVERSE Z1))))
57500 R3 (PRINT (QUOTE UNDEFINED-ARG-FOR-RESET:))
57600 (PRINC (CAR L))
57700 (TERPRI)
57800 (ERR NIL)
57900 R1 (SETQ X (QUOTE (X)))
58000 (SETQ L (CDR L))
58100 R4 (SETQ Z2 (CAR L))
58200 (COND ((ATOM Z2) (SETQ Z3 Z2)) (T (SETQ Z3 (CAR Z2))))
58300 SPQ2 (COND ((NOT (MEMQ Z3 STRATLIST)) (GO R3))
58400 ((EQ Z3 (QUOTE SUPPORT)) (SETQ XX (EVAL (CADAR L)))
58500 (PROG (ZZ)
58600 (GO B)
58700 A (SETQ ZZ (CONS (CDAR XX) ZZ))
58800 (SETQ XX (CDR XX))
58900 B (COND (XX (GO A)))
59000 (SETQ SUPPORT ZZ))
59100 (SETQ ZZ (QUOTE (SUPPORT C2))))
59200 ((EQ Z3 (QUOTE MODEL)) (SETQ PMODEL (CADAR L))
59300 (SETQ NMODEL (CADDAR L))
59400 (SETQ ZZ (CONS (CONS Z3 X) ZZ)))
59500 ((EQ Z3 (QUOTE ANCESTRY)) (SETQ ANCESTRY T))
59600 ((EQ Z3 (QUOTE ORDER)) (SETQ ORDER T))
59700 ((EQ Z3 (QUOTE MERGE)) (SETQ MERGE T))
59800 (T (SETQ ZZ (CONS (CONS Z3 X) ZZ))))
59900 (SETQ L (CDR L))
60000 (COND (L (GO R4)))
60100 (COND (ZZ (SETQ STRATEGY (QUOTE (LAMBDA (C1 C2) (SUPPORT C2))))) (T (SETQ STRATEGY NIL)))
60200 (GO R2)))
60300 FEXPR)
60400
60500 (DEFPROP SET1
60600 (LAMBDA(L)
60700 (PROG (TBL N)
60800 (SETQ N 1)
60900 (SETQ ZERO (CDAR (SETU (LIST (CONS 0 0)))))
61000 A (SETQ TBL (CONS (CONS (CAR L) N) TBL))
61100 (SETQ L (CDR L))
61200 (COND (L (SETQ N (ADD1 N)) (GO A)))
61300 (RETURN (SETU TBL))))
61400 EXPR)
61500
61600 (DEFPROP SET2
61700 (LAMBDA(C L)
61800 (PROG (X Z T1 T2 T3* T2* T3 Z1)
61900 (SETQ T2 (SETQ T2* (LIST NIL)))
62000 (SETQ T3 (SETQ T3* (LIST NIL)))
62100 (SETQ X (CDR C))
62200 S1 (SETQ Z (CDAR X))
62300 (SETQ T1 NIL)
62400 (COND ((NEG (CAR X)) (GO S2)))
62500 S1A (COND ((VAR (CAR Z)) (SETQ T1 (CONS ZERO T1)))
62600 ((SETQ Z1 (ASSOC (CAAR Z) L)) (SETQ T1 (CONS (CDR Z1) T1)))
62700 (T (RPLACD (LAST L) (SETU (LIST (CONS (CAAR Z) (ADD1 (LENGTH L))))))
62800 (SETQ T1 (CONS (CDAR (LAST L)) T1))))
62900 (SETQ Z (CDR Z))
63000 (COND (Z (GO S1A)))
63100 (SETQ X (CDR X))
63200 (RPLACD T2* (LIST (POTZ T1)))
63300 (SETQ T2* (CDR T2*))
63400 (COND (X (GO S1)))
63500 S4 (COND ((EQ T2 T2*) (RPLACA T3 (CDR T3))) (T (RPLACA T3 (CDR T2)) (RPLACD T2* (CDR T3))))
63600 (RPLACA (CAR C) (CONS (CAAR C) T3))
63700 (RETURN C)
63800 S2 (SETQ Z (CDDAR X))
63900 (SETQ T1 NIL)
64000 S2A (COND ((VAR (CAR Z)) (SETQ T1 (CONS ZERO T1)))
64100 ((SETQ Z1 (ASSOC (CAAR Z) L)) (SETQ T1 (CONS (CDR Z1) T1)))
64200 (T (RPLACD (LAST L) (SETU (LIST (CONS (CAAR Z) (ADD1 (LENGTH L))))))
64300 (SETQ T1 (CONS (CDAR (LAST L)) T1))))
64400 (SETQ Z (CDR Z))
64500 (COND (Z (GO S2A)))
64600 (SETQ X (CDR X))
64700 (RPLACD T3* (LIST (POTZ T1)))
64800 (SETQ T3* (CDR T3*))
64900 (COND (X (GO S2)))
65000 (GO S4)))
65100 EXPR)
65200
65300 (DEFPROP SET3
65400 (LAMBDA(Z)
65500 (PROG (E)
65600 (COND ((OR (NULL Z) (MEMQ NIL Z)) (RETURN Z)))
65700 (SETQ E Z)
65800 S1 (COND ((HERE (CAR E)) (SET2 (CAR E) TBL)))
65900 (SETQ E (CDR E))
66000 (COND (E (GO S1)))
66100 (RETURN Z)))
66200 EXPR)
66300
66400 (DEFPROP SETUP
66500 (LAMBDA(Z)
66600 (PROG (BL Z1 Z2 Z3 Z4 Z5)
66700 SET2 (SETQ Z3 (CAR Z))
66800 (SETQ Z2 0)
66900 (SETQ BL NIL)
67000 (SETQ NO* NO)
67100 (SETQ Z5 NIL)
67200 S1 (SETQ Z4 (MIN1 Z3))
67300 (COND ((NULL Z4) (GO S3)))
67400 (UPIT Z4)
67500 (COND ((MEMBER Z4 Z5) (GO S1)) ((POS Z4) (COND ((MEMBER (CONS ESCAPE Z4) Z5) (GO S4)))))
67600 (SETQ Z2 (ADD1 Z2))
67700 (SETQ Z5 (CONS Z4 Z5))
67800 (GO S1)
67900 S3 (SETQ Z3 NIL)
68000 (SETQ Z4 Z5)
68100 S2 (COND ((NEG (CAR Z4)) (SETQ Z3 Z4) (GO SET3)))
68200 (SETQ Z4 (CDR Z4))
68300 (COND (Z4 (GO S2)))
68400 SET3 (SETQ Z5 (CONS (CONS Z2 (CONS Z3 (CONS 0 (CONS AXNO AXNO)))) Z5))
68500 SET1 (SETQ Z1 (CONS Z5 Z1))
68600 S4 (SETQ Z (CDR Z))
68700 (COND (Z (GO SET2)))
68800 (RETURN Z1)))
68900 EXPR)
69000
69100 (DEFPROP SEARCH2
69200 (LAMBDA (X L L1) (PROG NIL (SETQ KR1 (ASSOC X L)) (COND (KR1 (RETURN (CDR KR1)))) (RETURN L1)))
69300 EXPR)
69400
69500 (DEFPROP S2
69600 (LAMBDA(X Y Z)
69700 (PROG (Z1)
69800 (SETQ Z1 (CDR Z))
69900 A (COND ((NULL Z1) (RETURN Z))
70000 ((VAR (CAR Z1)) (COND ((EQ (CAR Z1) Y) (RPLACA Z1 X))))
70100 ((CONST (CAR Z1)) NIL)
70200 (T (RPLACA Z1 (S2 X Y (CAR Z1)))))
70300 (SETQ Z1 (CDR Z1))
70400 (GO A)))
70500 EXPR)
70600
70700 (DEFPROP SETQUERY
70800 (LAMBDA (X) (SETQUERY2 X NIL NIL))
70900 EXPR)
71000
71100 (DEFPROP SETQUERY1
71200 (LAMBDA(XYZ XYZ1)
71300 (PROG (Z)
71400 (SETQ Z (ERRSET (SETQUERY2 XYZ XYZ1 T)))
71500 (COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (RETURN Z)))
71600 (RETURN (CONS (QUOTE NOPROOF) (CAR Z)))))
71700 EXPR)
71800
71900 (DEFPROP SETQUERY2
72000 (LAMBDA(XX YY FLG)
72100 (PROG (XYZ1 CHAN
72200 Z
72300 Z1
72400 SUPPORT
72500 EDITSTRAT
72600 MERGE
72700 ORDER
72800 DEBUG
72900 DEPTH
73000 LENGTH
73100 ANCESTRY
73200 STRATEGY
73300 PMODEL
73400 NMODEL
73500 PFLG
73600 PDEPTH
73700 DLIST)
73800 (SETQ CHAN (OUTC NIL NIL))
73900 (SETQ PFLG T)
74000 (COND (FLG (UPDATESTATE YY)))
74100 (SETQ XYZ1 XX)
74200 (COND ((NULL FLG) (GO SRA1)) ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
74300 (PRINT SETQMESS)
74400 (SETQ XX (UPDATE XX))
74500 (SETQ XYZ1 XX)
74600 SRA1 (COND ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
74700 (PRINT (QUOTE HERE-ARE-THE-CLAUSES:))
74800 (SETQ N 1)
74900 AA (CLAUSES XX)
75000 SRA (COND ((AND AUTO (NULL FLG)) (SETQ Z (AUTO XYZ1)) (OUTC CHAN NIL) (RETURN Z))
75100 (AUTO (PRINT (QUOTE (STILL-AUTO (Y / N))))
75200 (COND
75300 ((EQ (READ) (QUOTE Y)) (SETQ Z (CONS XYZ1 (AUTO XYZ1))) (OUTC CHAN NIL) (RETURN Z)))))
75400 SR2A (PRINT (QUOTE THE-FOLLOWING-BUILTIN-STRATEGIES-ARE-AVAILABLE:))
75500 (PRINT
75600 (QUOTE "ANCESTRY VINE UNIT MODEL[POS ; NEG] DEFMODEL[NAME] P1 P2
75700 SUPPORT[#,..] EQUALITY[ID,#] "))
75800 (PRINT (QUOTE CHOICE-STRATEGY-IS:))
75900 (COND
76000 (FLG (OUTIT SAVESTR)
76100 (PRINT (QUOTE DO-YOU-WANT-TO-CHANGE-IT))
76200 (SETQ Z (READ))
76300 (COND ((EQ Z (QUOTE N)) (GO SRB)))))
76400 (SCANSET)
76500 (START)
76600 (SETQ Z (ERRSET (<ST>) T))
76700 (SCANRESET)
76800 (COND ((OR (NULL Z) (NULL (CAR Z))) (PRINT (QUOTE SCREWED-STRATEGY)) (GO SR2A)))
76900 (SETQ ZIN (TOP))
77000 (SETQ STRATEGY (BUILTCH ZIN))
77100 (OUTIT ZIN)
77200 (SETQ SAVESTR ZIN)
77300 SRB (SETQ DEBUG T)
77400 SRAA (PRINT (QUOTE EDIT-STRATEGY-IS:))
77500 (COND
77600 (FLG (OUTIT (CAR (LAST EDITSTRAT)))
77700 (PRINT (QUOTE DO-YOU-WANT-TO-CHANGE-IT))
77800 (SETQ Z (READ))
77900 (COND ((EQ Z (QUOTE N)) (GO SRCA)))))
78000 (SCANSET)
78100 (START)
78200 (SETQ Z1 (ERRSET (<ST>) T))
78300 (SCANRESET)
78400 (COND ((OR (NULL Z1) (NULL (CAR Z1))) (PRINT (QUOTE SCREWED-EDIT-STRATEGY)) (GO SRAA)))
78500 (SETQ ZIN (TOP))
78600 (SETQ SAVEED ZIN)
78700 (SETQ EDITSTRAT (BUILTED ZIN))
78800 (OUTIT ZIN)
78900 SRCA (SETQ UFLG T)
79000 (SETQ Z1
79100 (LIST STRATEGY
79200 SUPPORT
79300 EDITSTRAT
79400 MERGE
79500 ORDER
79600 DEBUG
79700 DEPTH
79800 LENGTH
79900 ANCESTRY
80000 PMODEL
80100 NMODEL
80200 PFLG
80300 EQUAL
80400 PDEPTH
80500 DLIST))
80600 (OUTC CHAN NIL)
80700 (COND (FLG (RETURN (CONS XYZ1 Z1))) (T (RETURN Z1)))))
80800 EXPR)
80900
81000 (DEFPROP SETSUP
81100 (LAMBDA(X)
81200 (PROG (Z)
81300 (SETQ X (*CL X))
81400 A (COND ((NULL X) (SETQ SUPPORT Z) (RETURN NIL)))
81500 (SETQ Z (CONS (CDAR X) Z))
81600 (SETQ X (CDR X))
81700 (GO A)))
81800 EXPR)
81900
82000 (DEFPROP SUBS3TA
82100 (LAMBDA(L Z XX TS)
82200 (PROG (X1 X2 X3 Z4)
82300 (SETQ X1 (LIST (CAR Z)))
82400 (SETQ X2 X1)
82500 (GO SUB2)
82600 SUB1 (RPLACD X2 (LIST X3))
82700 (SETQ X2 (CDR X2))
82800 SUB2 (SETQ Z (CDR Z))
82900 (SETQ Z4 (CAR Z))
83000 (COND ((NULL Z) (RETURN X1))
83100 ((EQ Z XX) (SETQ X3 TS) (GO SUB1))
83200 ((VAR Z4) (SETQ X3 (SEARCH Z4 L)) (GO SUB1))
83300 ((CONST Z4) (SETQ X3 Z4) (GO SUB1))
83400 (T (SETQ X3 (SUBS3TA L Z4 XX TS)) (GO SUB1)))))
83500 EXPR)
83600
83700 (DEFPROP SUBS3T**
83800 (LAMBDA (L X) (COND ((NULL L) (SUBS3T (QUOTE ((-11 . -1))) X)) (T (SUBS3T L X))))
83900 EXPR)
84000
84100 (DEFPROP SUB*
84200 (LAMBDA(X L)
84300 (PROG (S2 Z L1)
84400 B (SETQ L1 L)
84500 A (SETQ S2 (CDADAR L1))
84600 (SETQ Z (UNI (LIST (CAR S2)) (LIST (CAAR X)) NIL))
84700 (COND (Z (RPLACA (CAR X) (CADR (SUBS3T* Z (CONS NIL (CDR S2)))))))
84800 (SETQ L1 (CDR L1))
84900 (COND (L1 (GO A)))
85000 (SETQ X (CDR X))
85100 (COND (X (GO B)))))
85200 EXPR)
85300
85400 (DEFPROP SUBSKOL
85500 (LAMBDA (C EXL) (SUBS3T EXL C))
85600 EXPR)
85700
85800 (DEFPROP SUPPORT
85900 (LAMBDA (X) (PROG NIL (COND ((NOT (EQ LVL 1)) (RETURN T)) (T (RETURN (MEMBER (CDR X) SUPPORT))))))
86000 EXPR)
86100
86200 (DEFPROP SUBSUME1
86300 (LAMBDA(C CB D DB L)
86400 (PROG (Z)
86500 SUB5 (COND ((NEG (CAR C)) (GO SUB3))
86600 ((NEG (CAR D)) (RETURN NIL))
86700 ((EQ (CAAR C) (CAAR D)) (GO SUB1))
86800 ((ORDERP (CAAR C) (CAAR D)) (RETURN NIL))
86900 (T (GO SUB2)))
87000 SUB1 (COND ((UNIAB (CAR CB) (CAR DB)) (SETQ Z (UNI (CDAR C) (CDAR D) L))) (T (GO SUB2)))
87100 SUB4 (COND ((NULL Z) (GO SUB2)) ((NULL (CDR C)) (RETURN T)) ((SUBSUME1 (CDR C) (CDR CB) D DB Z) (RETURN T)))
87200 SUB2 (SETQ D (CDR D))
87300 (COND (D (SETQ DB (CDR DB)) (GO SUB5)))
87400 (RETURN NIL)
87500 SUB3 (COND
87600 ((NEG (CAR D))
87700 (COND ((EQ (CADAR C) (CADAR D))
87800 (COND ((UNIAB (CAR CB) (CAR DB)) (SETQ Z (UNI (CDDAR C) (CDDAR D) L)) (GO SUB4))
87900 (T (GO SUB2))))
88000 ((ORDERP (CADAR C) (CADAR D)) (RETURN NIL))
88100 (T (GO SUB2)))))
88200 (SETQ D (CDR D))
88300 (COND (D (SETQ DB (CDR DB)) (GO SUB3)))
88400 (RETURN NIL)))
88500 EXPR)
88600
88700 (DEFPROP SUBS2T
88800 (LAMBDA(X Y Z)
88900 (PROG (U Z1)
89000 (COND ((EQ X Y) (RETURN Z)))
89100 (SETQ U (CDR Z))
89200 (GO S2)
89300 S1 (SETQ Z1 (CDAR U))
89400 (COND ((VAR Z1) (COND ((EQ Y Z1) (RPLACD (CAR U) X))))
89500 ((CONST Z1) NIL)
89600 (T (RPLACD (CAR U) (S2 X Y Z1))))
89700 (SETQ U (CDR U))
89800 S2 (COND (U (GO S1)))
89900 (RPLACD Z (CONS (CONS Y (COND ((OR (VAR X) (CONST X)) X) (T (COPY X)))) (CDR Z)))
90000 (RETURN Z)))
90100 EXPR)
90200
90300 (DEFPROP SUBS3T
90400 (LAMBDA (L X) (COND ((NEG X) (CONS ESCAPE (SUBS3T* L (CDR X)))) (T (SUBS3T* L X))))
90500 EXPR)
90600
90700 (DEFPROP SUBSUME
90800 (LAMBDA(C D)
90900 (COND ((OR (AND (ALLPOS C) (ALLNEG D)) (AND (ALLNEG C) (ALLPOS D))) NIL)
91000 ((OR (NOT (HERE C)) (NOT (HERE D))) NIL)
91100 ((NOT (GREATERP (NUM C) (NUM D))) (SUBSUME1 (CDR C) (POSBIT C) (CDR D) (POSBIT D) NIL))
91200 (T NIL)))
91300 EXPR)
91400
91500 (DEFPROP SUBSUME*
91600 (LAMBDA (C D) (PROG NIL (RETURN (SUBSUME1 (CDR C) (POSBIT C) (CDR D) (POSBIT D) NIL))))
91700 EXPR)
91800
91900 (DEFPROP SUBST1
92000 (LAMBDA(X Y Z)
92100 (COND ((ATOM Z) (COND ((EQ Y Z) X) (T Z)))
92200 ((EQUAL Y Z) X)
92300 (T (CONS (SUBST1 X Y (CAR Z)) (SUBST1 X Y (CDR Z))))))
92400 EXPR)
92500
92600 (DEFPROP TCOPY
92700 (LAMBDA (X) (COND ((NULL X) NIL) ((VAR (CAR X)) (TCOPY (CDR X))) (T (CONS X (TCOPY (CDR X))))))
92800 EXPR)
92900
93000 (DEFPROP TERMS
93100 (LAMBDA (X Y Z) (CDR (TERMS2 X Y Z)))
93200 EXPR)
93300
93400 (DEFPROP TERMS1
93500 (LAMBDA(L N)
93600 (COND ((OR (ZEROP N) (NULL L)) NIL)
93700 ((OR (VAR (CAR L)) (CONST (CAR L))) (CONS L (TERMS1 (CDR L) N)))
93800 (T (NCONC (LIST L) (TERMS1 (CDAR L) (SUB1 N)) (TERMS1 (CDR L) (SUB1 N))))))
93900 EXPR)
94000
94100 (DEFPROP TERMS2
94200 (LAMBDA(Z L N)
94300 (PROG (Z1 T1 T2)
94400 (SETQ T2 (SETQ T1 (LIST NIL)))
94500 A (COND ((NULL L) (RETURN T1))
94600 ((VAR (CAR L)) (GO B))
94700 ((CONST (CAR L)) (COND ((EQ Z (CAAR L)) (RPLACD T2 (LIST L)) (SETQ T2 (CDR T2)))) (GO B))
94800 ((EQ N 1) (GO B)))
94900 (SETQ Z1 (TERMS2 Z (CDAR L) (SUB1 N)))
95000 (COND ((EQ (CAAR L) Z) (RPLACD T2 (LIST L)) (SETQ T2 (CDR T2))))
95100 (COND ((CDR Z1) (RPLACD T2 (CDR Z1)) (SETQ T2 (LAST T2))))
95200 B (SETQ L (CDR L))
95300 (GO A)))
95400 EXPR)
95500
95600 (DEFPROP TIMEIT
95700 (LAMBDA NIL (DIFFERENCE (DIFFERENCE (TIME) (GCTIME)) TIME1))
95800 EXPR)
95900
96000 (DEFPROP TREE
96100 (LAMBDA(L)
96200 (COND ((ATOM (CDR (ANCESTOR L))) (LIST L))
96300 (T (NCONC (LIST L) (TREE (CAR (ANCESTOR L))) (TREE (CDR (ANCESTOR L)))))))
96400 EXPR)
96500
96600 (DEFPROP TREEDEP
96700 (LAMBDA(X)
96800 (PROG (Z)
96900 (SETQ Z (ANCESTOR X))
97000 (COND ((ATOM (CDR Z)) (RETURN 0)) (T (RETURN (ADD1 (MAX (TREEDEP (CAR Z)) (TREEDEP (CDR Z)))))))))
97100 EXPR)
97200
97300 (DEFPROP TRY
97400 (LAMBDA (L) (PROG (AUTO) (EVAL (CONS (QUOTE TRY1) L))))
97500 FEXPR)
97600
97700 (DEFPROP TRY1
97800 (LAMBDA(L)
97900 (PROG (FILENAM PRNO POTZTBL NEWNAME TBL TIME1 Z Z2 AXNO)
98000 (SETQ PRNO 0)
98100 T2 (COND ((NULL L) (SETQ FILENAM (QUOTE (P R F))) (GO P3)))
98200 (SETQ Z (CAR (LAST L)))
98300 (SETQ FILENAM (EXPLODE (COND ((ATOM Z) Z) (T (CAR Z)))))
98400 (EVAL (CONS (QUOTE INPUT) L))
98500 (INC T)
98600 P3 B (SETQ Z2 (INCLAUSES))
98700 (INC NIL)
98800 (COND ((NULL Z2) (RETURN NIL)))
98900 (SETQ TIME1 (DIFFERENCE (TIME) (GCTIME)))
99000 (SETQ Z2 (ATTEMPT Z2 NIL NIL))
99100 A (COND ((OR (NULL Z2) (EQ (CAR Z2) (QUOTE QED))) (RETURN (QUOTE *)))
99200 ((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL)))
99300 ((EQ (CAR Z2) (QUOTE ABORT))
99400 (SETQ Z2 (ATTEMPT (INITIALAX1 (APPEND (CADR Z2) (CDDR Z2))) NIL NIL))))
99500 (GO A)))
99600 FEXPR)
99700
99800 (DEFPROP TRYIT
99900 (LAMBDA NIL
00100 (PROG (Z1 Z2 R M)
00200 (SETQ CNT (ADD1 (LENGTH CLAUSES)))
00300 (SETQ EE (CDR EE))
00400 TRY3 (SETQ Z1 (CAR EE))
00500 (COND ((NOT (HERE Z1)) (GO TRY7)))
00600 (SETQ M (CHOICE Z1))
00700 (COND ((NULL M) (GO TRY7)))
00800 TRY2 (SETQ Z2 (CAR M))
00900 (COND ((NOT (HERE Z1)) (GO TRY7)) ((NOT (HERE Z2)) (GO TRY8)))
01000 TRY1 TRY1A
01100 (COND ((AND (ALLPOS Z1) (ALLPOS Z2)) (GO TRY6)))
01200 (SETQ R (RESOLVE Z1 Z2))
01300 (COND ((NULL R) (GO TRY6)) ((MEMQ NIL R) (PROOF Z1 Z2) (RETURN (QUOTE QED))))
01400 (SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
01500 TRY6 (COND ((OR PFLG (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY8)))
01600 (SETQ R (PARMOD Z1 Z2))
01700 (COND ((NULL R) (GO TRY8)))
01800 (SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
01900 TRY8 (COND ((TTYIN) (UPDATE CLAUSES)))
02000 (SETQ M (CDR M))
02100 (COND (M (GO TRY2)))
02200 TRY7 (SETQ EE (CDR EE))
02300 (COND ((NOT (EQ EE (CDR EE1))) (GO TRY3)))
02400 (PRINT (QUOTE COUNT))
02500 (PRINT COUNT)
02600 (PRINT (QUOTE LEVEL))
02700 (PRINT LVL)
02800 (SETQ LVL (ADD1 LVL))
02900 (PRINT (QUOTE ELAPSED-TIME))
03000 (PRINT (TIMEIT))
03100 (COND ((CDR EE1) (SETQ EE1 (LAST EE1)) (GO TRY3)))
03200 (PRINT (QUOTE NO-PROOF-FOUND))
03300 (COND (AUTO (ERR (QUOTE NOPROOF))))
03400 (UPDATE CLAUSES)
03500 (COND ((CDR EE1) (SETQ EE (CDR EE1)) (SETQ EE1 (LAST EE1)) (GO TRY3)))
03600 (ERR (QUOTE NOPROOF))))
03700 EXPR)
03800
03900 (DEFPROP TRAVERSE
04000 (LAMBDA(L)
04100 (PROG (Z Z1 Z2)
04200 (SETQ Z (ANCESTOR L))
04300 (SETQ Z1 (CAR Z))
04400 (SETQ Z (CDR Z))
04500 (COND ((NOT (ATOM (CDR (ANCESTOR Z)))) (SETQ Z2 (TRAVERSE Z))))
04600 (COND ((NOT (ATOM (CDR (ANCESTOR Z1)))) (SETQ Z2 (NCONC (TRAVERSE Z1) Z2))))
04700 (RETURN (COND ((HERE L) (CONS L Z2)) (T Z2)))))
04800 EXPR)
04900
05000 (DEFPROP UNIT
05100 (LAMBDA (X) (EQ (NUM X) 1))
05200 EXPR)
05300
05400 (DEFPROP UNITS
05500 (LAMBDA(U)
05600 (PROG (Z Z1)
05700 (COND ((NULL U) (RETURN NIL)))
05800 (SETQ Z U)
05900 UN1 (COND ((EQ (NUM (CAR Z)) 1) (SETQ Z1 (CONS (CAR Z) Z1))))
06000 (SETQ Z (CDR Z))
06100 (COND (Z (GO UN1)))
06200 (RETURN Z1)))
06300 EXPR)
06400
06500 (DEFPROP UNITRES
06600 (LAMBDA(C UP UN)
06700 (PROG (C1 Z1 U Z RES)
06800 (SETQ C1 C)
06900 (COND ((AND (ALLPOS C) (NULL UN)) (RETURN NIL)) ((AND (ALLNEG C) (NULL UP)) (RETURN NIL)))
07000 (COND
07100 ((UNIT C)
07200 (RETURN
07300 (COND ((ALLPOS C) (RESUNITP (CAADR C) (CDADR C) UN)) (T (RESUNITN (CADADR C) (CDDADR C) UP))))))
07400 (COND ((NULL UN) (SETQ C (NEGL C)) (GO N)))
07500 (SETQ C (CDR C))
07600 B (SETQ Z1 (CAR C))
07700 (COND ((NEG Z1) (GO N)))
07800 (SETQ U UN)
07900 A (COND ((NOT (EQ (CAR Z1) (CADADR (CAR U)))) (GO A1)))
08000 (SETQ Z (UNI (CDDADR (CAR U)) (CDR Z1) NIL))
08100 (COND ((NULL Z) (GO A1)))
08200 (COND ((NULL Z) (GO A1)) ((UNIT C1) (RETURN (LIST NIL))))
08300 (SETQ RES (CONS (REDUCER C1 C) RES))
08400 (GO A2)
08500 A1 (SETQ U (CDR U))
08600 (COND (U (GO A)))
08700 A2 (SETQ C (CDR C))
08800 (COND (C (GO B)) (T (RETURN RES)))
08900 N (SETQ Z1 (CDAR C))
09000 (SETQ U UP)
09100 C (COND ((NULL U) (RETURN RES)))
09200 C2 (COND ((NOT (EQ (CAR Z1) (CAADAR U))) (GO C1)))
09300 (SETQ Z (UNI (CDADAR U) (CDR Z1) NIL))
09400 (COND ((NULL Z) (GO C1)) ((UNIT C1) (RETURN (LIST NIL))))
09500 (SETQ RES (CONS (REDUCER C1 C) RES))
09600 (GO C3)
09700 C1 (SETQ U (CDR U))
09800 (COND (U (GO C2)))
09900 C3 (SETQ C (CDR C))
10000 (COND (C (GO N)) (T (RETURN RES)))))
10100 EXPR)
10200
10300 (DEFPROP UNITREDUCT
10400 (LAMBDA(R UP UN)
10500 (PROG (Z UP1 UN1 C1 C2 RC1 RC2)
10600 (SETQ UN1 (SETQ UP1 NIL))
10700 (SETQ C1 (SETQ C2 R))
10800 A (SETQ RC1 (SETQ RC2 NIL))
10900 (COND ((NULL C2) (GO C1)) ((AND (NULL UP1) (NULL UN1)) (GO C)))
11000 B (SETQ Z (UNITRES (CAR C2) UP1 UN1))
11100 (COND ((NULL Z) (SETQ RC2 (CONS (CAR C2) RC2)))
11200 ((NULL (CAR Z)) (RETURN (LIST NIL)))
11300 (T (SETQ RC1 (APPEND Z RC1))))
11400 (SETQ C2 (CDR C2))
11500 (COND (C2 (GO B)))
11600 C1 (SETQ UP (APPEND UP1 UP))
11700 (SETQ UN (APPEND UN1 UN))
11800 C (SETQ Z (UNITRES (CAR C1) UP UN))
11900 (COND ((NULL Z) (SETQ RC2 (CONS (CAR C1) RC2)))
12000 ((NULL (CAR Z)) (RETURN (LIST NIL)))
12100 (T (SETQ RC1 (APPEND Z RC1))))
12200 (SETQ C1 (CDR C1))
12300 (COND (C1 (GO C)))
12400 (COND ((NULL RC1) (RETURN RC2)))
12500 (SETQ C2 RC2)
12600 (SETQ C1 RC1)
12700 (SETQ Z (UNITPN C1))
12800 (COND ((AND (NULL (CAR Z)) (NULL (CDR Z))) (RETURN (APPEND RC1 RC2))))
12900 (SETQ UP1 (CAR Z))
13000 (SETQ UN1 (CDR Z))
13100 (GO A)))
13200 EXPR)
13300
13400 (DEFPROP UNITPN
13500 (LAMBDA(X)
13600 (PROG (P N)
13700 A (COND
13800 ((UNIT (CAR X)) (COND ((ALLPOS (CAR X)) (SETQ P (CONS (CAR X) P))) (T (SETQ N (CONS (CAR X) N))))))
13900 (SETQ X (CDR X))
14000 (COND (X (GO A)))
14100 (RETURN (CONS P N))))
14200 EXPR)
14300
14400 (DEFPROP UNIFY
14500 (LAMBDA(X Y)
14600 (PROG (LC Z1 Z2 Z3 Z4 Z6 Z7)
14700 (SETQ LC (LIST NIL))
14800 U3 (SETQ Z1 (CAR X))
14900 (SETQ Z2 (CAR Y))
15000 (COND ((VAR Z1) (SETQ Z3 (SEARCH Z1 (CDR LC)))) (T (SETQ Z3 Z1)))
15100 (COND ((VAR Z2) (SETQ Z4 (SEARCH Z2 (CDR LC)))) (T (SETQ Z4 Z2)))
15200 (COND ((VAR Z3)
15300 (COND ((VAR Z4) (GO UN1))
15400 ((CONST Z4) (GO UN3))
15500 (T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z3 (COPY Z4)))) (GO UN2))
15600 ((NOT (VAR Z2)) (SETQ Z4 (SUBS3T* (CDR LC) Z4))))
15700 (COND ((OCCUR Z3 (CDR Z4)) (RETURN NIL)) (T (GO UN3))))))
15800 ((VAR Z4)
15900 (COND ((CONST Z3) (GO UN1))
16000 (T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z4 (COPY Z3)))) (GO UN2))
16100 ((NOT (VAR Z1)) (SETQ Z3 (SUBS3T* (CDR LC) Z3))))
16200 (COND ((OCCUR Z4 (CDR Z3)) (RETURN NIL)) (T (GO UN1))))))
16300 ((AND (CONST Z3) (CONST Z4)) (COND ((NOT (EQ (CAR Z3) (CAR Z4))) (RETURN NIL)) (T (GO UN2))))
16400 ((EQ (CAR Z3) (CAR Z4)) (SETQ Z6 (CDR (SUBS3T* (CDR LC) Z3)))
16500 (SETQ Z7 (CDR (SUBS3T* (CDR LC) Z4)))
16600 (SETQ X (APPEND Z6 (CDR X)))
16700 (SETQ Y (APPEND Z7 (CDR Y)))
16800 (GO U3))
16900 (T (RETURN NIL)))
17000 UN1 (SUBS2T Z3 Z4 LC)
17100 UN2 (SETQ X (CDR X))
17200 (COND (X (SETQ Y (CDR Y)) (GO U3)))
17300 (RETURN LC)
17400 UN3 (SUBS2T Z4 Z3 LC)
17500 (GO UN2)))
17600 EXPR)
17700
17800 (DEFPROP UNI
17900 (LAMBDA(C D L)
18000 (PROG (Z1 Z2 Z3)
18100 UN2 (SETQ Z2 (CAR D))
18200 (SETQ Z1 (SETQ Z3 (CAR C)))
18300 (COND
18400 ((VAR Z1) (SETQ Z3 (SEARCH1 Z1 L))
18500 (COND ((NULL Z3) (SETQ L (CONS (CONS Z1 Z2) L)) (GO UN1))
18600 ((VAR Z3) (COND ((EQ Z3 Z2) (GO UN1)) (T (RETURN NIL)))))))
18700 (COND ((VAR Z2) (RETURN NIL))
18800 ((CONST Z2) (COND ((EQ (CAR Z2) (CAR Z3)) (GO UN1)) (T (RETURN NIL))))
18900 ((VAR Z1) (COND ((EQUAL Z2 Z3) (GO UN1)) (T (RETURN NIL))))
19000 ((EQ (CAR Z2) (CAR Z3)) (SETQ C (APPEND (CDR Z3) (CDR C)))
19100 (SETQ D (APPEND (CDR Z2) (CDR D)))
19200 (GO UN2))
19300 (T (RETURN NIL)))
19400 UN1 (SETQ C (CDR C))
19500 (COND (C (SETQ D (CDR D)) (GO UN2)))
19600 (COND (L (RETURN L)) (T (RETURN (LIST (CONS 64 64)))))))
19700 EXPR)
19800
19900 (DEFPROP UNION
20000 (LAMBDA(Z C D YC YD)
20100 (PROG (BL L Z1 Z2 Z3 Z4 Z5 Z6 C1 C2 NEG RES M1 Z7 Z8)
20200 (SETQ NO* NO)
20300 (COND
20400 (ORDER (COND (ANCESTRY (SETQ SAT C) (SETQ L YC)) ((EQ C SAT) (SETQ L YC)) (T (SETQ L YD)))
20500 (COND ((< L (CDR SAT)) (RETURN NIL)))))
20600 (SETQ M1 0)
20700 (SETQ Z7 (ANCESTOR C))
20800 (SETQ Z8 (ANCESTOR D))
20900 (SETQ C (CDR C))
21000 (SETQ D (CDR D))
21100 (SETQ Z1 Z)
21200 (SETQ Z2 Z)
21300 (SETQ Z3 (SUBS3T** Z1 YC))
21400 (SETQ Z4 (SUBS3T** Z2 YD))
21500 UN1 (SETQ Z5 (SUBS3T** Z1 (CAR C)))
21600 (COND ((OR (EQUAL Z3 Z5) (MEMC Z5 C1)) (SETQ M1 (ADD1 M1)) (GO UN1A))
21700 ((AND (NEG Z5) (MEMC (CDR Z5) C1)) (RETURN NIL)))
21800 (SETQ C1 (CONS Z5 C1))
21900 UN1A (SETQ C (CDR C))
22000 (COND (C (GO UN1)))
22100 UN2 (SETQ Z6 (SUBS3T** Z2 (CAR D)))
22200 (COND ((AND PARRES (EQUAL Z4 Z6)) (SETQ Z6 PARRES) (GO UN2B))
22300 ((OR (EQUAL Z4 Z6) (MEMC Z6 C2)) (SETQ M1 (ADD1 M1)) (GO UN2A))
22400 ((NEG Z6) (COND ((OR (MEMC (CDR Z6) C1) (MEMC (CDR Z6) C2)) (RETURN NIL))))
22500 ((POS Z6) (COND ((MEMBER (CONS ESCAPE Z6) C1) (RETURN NIL)))))
22600 UN2B (SETQ C2 (CONS Z6 C2))
22700 UN2A (SETQ D (CDR D))
22800 (COND (D (GO UN2)))
22900 (SETQ Z2 0)
23000 (COND ((NULL C1) (COND ((NULL C2) (RETURN (LIST NIL))) (T (SETQ Z1 C2) (GO UN7))))
23100 ((NULL C2) (SETQ Z1 C1) (GO UN7)))
23200 (COND ((AND MERGE (EQ M1 2) (CDR Z7) (CDR Z8)) (RETURN NIL)))
23300 UN5 (SETQ NEG RES)
23400 (COND ((NULL C1) (SETQ Z1 C2) (GO UN7))
23500 ((NULL C2) (SETQ Z1 C1) (GO UN7))
23600 ((AND (POS (CAR C1)) (POS (CAR C2))) (GO UN3))
23700 ((AND (POS (CAR C1)) (NEG (CAR C2))) (GO UN6))
23800 ((OR (AND (NEG (CAR C1)) (POS (CAR C2))) (NOT (ORDERP (CADAR C1) (CADAR C2))))
23900 (SETQ Z1 (CAR C1))
24000 (SETQ C1 (CDR C1))
24100 (GO UN4)))
24200 UN6 (SETQ Z1 (CAR C2))
24300 (SETQ C2 (CDR C2))
24400 UN4 (UPIT Z1)
24500 (COND ((MEMBER Z1 RES) (GO UN5)) (T (SETQ Z2 (ADD1 Z2)) (SETQ RES (CONS Z1 RES)) (GO UN5)))
24600 UN7 (COND ((NULL Z1) (RETURN (LIST (CONS (LIST Z2 NEG) RES)))) ((MEMBER (CAR Z1) RES) (GO UN8)))
24700 (SETQ Z2 (ADD1 Z2))
24800 (UPIT (CAR Z1))
24900 (SETQ RES (CONS (CAR Z1) RES))
25000 (COND ((NEG (CAR Z1)) (SETQ NEG RES)))
25100 UN8 (SETQ Z1 (CDR Z1))
25200 (GO UN7)
25300 UN3 (COND ((NOT (ORDERP (CAAR C1) (CAAR C2))) (SETQ Z1 (CAR C1)) (SETQ C1 (CDR C1)) (GO UN4A)))
25400 (SETQ Z1 (CAR C2))
25500 (SETQ C2 (CDR C2))
25600 UN4A (UPIT1 (CDR Z1))
25700 (COND ((MEMBER Z1 RES) (GO UN5A)))
25800 (SETQ Z2 (ADD1 Z2))
25900 (SETQ RES (CONS Z1 RES))
26000 UN5A (COND ((NULL C1) (SETQ Z1 C2) (GO UN7)) ((NULL C2) (SETQ Z1 C1) (GO UN7)))
26100 (GO UN3)))
26200 EXPR)
26300
26400 (DEFPROP UNWIND
26500 (LAMBDA(X1 X2 Y Z N)
26600 (PROG (Z1 Z2)
26700 (SETQ Z2 (ASSOC1 X1 Z))
26800 (COND (Z2 (SETQ Z1 (CDR Z2)) (GO A)))
26900 (NCONC Y (COPYDELETED X1))
27000 (NCONC Z (LIST (CONS (LAST Y) N)))
27100 (SETQ Z1 N)
27200 (SETQ N (ADD1 N))
27300 A (SETQ Z2 (ASSOC1 X2 Z))
27400 (COND (Z2 (RETURN (CONS (CONS Z1 (CDR Z2)) N))))
27500 (NCONC Y (COPYDELETED X2))
27600 (NCONC Z (LIST (CONS (LAST Y) N)))
27700 (RETURN (CONS (CONS Z1 N) (ADD1 N)))))
27800 EXPR)
27900
28000 (DEFPROP UPDATE
28100 (LAMBDA(E)
28200 (PROG (USINGFL USING
28300 CHAN1
28400 ELOC
28500 CHAN
28600 AUTO
28700 DL1
28800 RF
28900 XYZ
29000 XYZ1
29100 CMD
29200 LOCFLG
29300 Z
29400 Z1
29500 Z2
29600 INCT
29700 Z3
29800 UEX
29900 Z1R
30000 Z2R
30100 N1
30200 R
30300 N
30400 NAME
30500 NAMELIST
30600 ZZ)
30700 (SETQ CHAN (OUTC NIL NIL))
30800 (SETQ AXNO (QUOTE INSERT))
30900 (SETQ FNNAM (QUOTE EDI))
31000 (SETQ NAMELIST (CONS (CONS (QUOTE CLAUSES) E) (CONS (CONS (QUOTE DLIST) DLIST) NEWNAME)))
31100 (SETQ N1 (LAST NAMELIST))
31200 (SETQ INCT (INC NIL))
31300 U9 (SETQ ELOC E)
31400 (SETQ N 1)
31500 U3 (UP1A (CAR ELOC) N)
31600 U3A (TERPRI)
31700 U3AA (SETQ CMD (READ))
31800 (COND ((EQ CMD (QUOTE ;)) (GO U3AA)))
31900 U3B (COND ((NOT (ATOM CMD)) (GO UER2)))
32000 U3C (SETQ CMD (EXPLODE CMD))
32100 (COND ((EQ (LENGTH CMD) 1) (GO UER1))
32200 ((SETQ Z (ASSOC (READLIST (LIST (CAR CMD) (CADR CMD))) GOLIST)) (GO (CDR Z))))
32300 UER1 (PRINT (QUOTE ILLEGAL-COMMAND))
32400 (GO U3A)
32500 UER2 (PRINT (QUOTE IMPROPER-SYNTAX))
32600 (GO U3A)
32700 UDI1 (SETQ Z1 (UPGETL E NAMELIST))
32800 (COND ((NULL Z1) (GO U3A)))
32900 (CLAUSES Z1)
33000 (GO U3A)
33100 USY1 (PRINT (QUOTE THE-ENTRIES-ARE:))
33200 (SETQ Z NAMELIST)
33300 USY2 (COND ((MEMQ (CAAR Z) (QUOTE (NIL %% %INITIAL %USING))) NIL) (T (PRINT (CAAR Z))))
33400 (SETQ Z (CDR Z))
33500 (COND (Z (GO USY2)))
33600 (GO U3A)
33700 UFL2 (SETQ Z (QUOTE U))
33800 (GO UFL4)
33900 UFL3 (SETQ Z (QUOTE D))
34000 (GO UFL4)
34100 UFL1 (SETQ Z (CAR (EXPLODE (READ))))
34200 UFL4 (SETQ Z2 405104)
34300 (COND ((EQ Z (QUOTE U)) (GO U8)) ((EQ Z (QUOTE D)) (GO U7)) (T (GO UER1)))
34400 UCH1 (SETQ Z (SETQUERY1 (CONS NIL CLAUSES) STRAT))
34500 (COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (GO U3A)))
34600 (UPDATESTATE (CDDR Z))
34700 (GO U3A)
34800 UDE1 (SETQ Z2 (UPGETL E NAMELIST))
34900 (COND ((NULL Z2) (GO U3A)))
35000 (EXPUNGE Z2)
35100 (GO U3A)
35200 UIN1 (SETQ NAME (READ))
35300 (SETQ Z2 (UPGETL E NAMELIST))
35400 (COND ((NULL Z2) (GO U3A)))
35500 UIN1A
35600 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) NIL) (T (GO USE2)))
35700 (NCONC Z1 Z2)
35800 (GO U3A)
35900 USU1 (SETQ Z1 (ERRSET (GETTERMS)))
36000 (COND ((NULL Z1) (PRINT (QUOTE HACK-IN-SUBSTITUTION-RETURNING-TO-LISTEN-LOOP)) (GO U3A))
36100 ((NULL (CAR Z1)) (GO U3A)))
36200 (SETQ Z3 NIL)
36300 (SETQ Z1 (CAR Z1))
36400 USU2 (SETQ Z3 (CONS (SUBST1 XYZ XYZ1 (CDAR Z1)) Z3))
36500 (SETQ Z1 (CDR Z1))
36600 (COND (Z1 (GO USU2)) (T (SETQ NAME (QUOTE ASSERT)) (SETQ Z2 (SETUP Z3)) (GO UIN1A)))
36700 UUP1 (SETQ Z2 (READ))
36800 (COND ((AND (NUMBERP Z2) (EQ (READ) (QUOTE ;))) (GO U8)) (T (GO UER2)))
36900 UDO1 (SETQ Z2 (READ))
37000 (COND ((AND (NUMBERP Z2) (EQ (READ) (QUOTE ;))) (GO U7)) (T (GO UER2)))
37100 UAN1 (SETQ Z2 (UPGETL E NAMELIST))
37200 UAN2 (COND (Z2 (PROOF1 (CAR Z2))) (T (GO U3A)))
37300 (SETQ Z2 (CDR Z2))
37400 (GO UAN2)
37500 UTE1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z NIL)) (T (SETQ Z (UPGETL E NAMELIST))))
37600 (INC INCT)
37700 (OUTC CHAN NIL)
37800 (SETQ DLIST (GETNAME (QUOTE DLIST) NAMELIST))
37900 (SETQ Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))
38000 (RETURN (MINIMIZE (APPEND Z1 Z)))
38100 USA1 (SETQ Z2 (UPGETL E NAMELIST))
38200 (COND (Z2 (NCONC E Z2)))
38300 (GO U3A)
38400 UPA1 (SETQ Z1 (UPGETL E NAMELIST))
38500 (SETQ Z2 (UPGETL E NAMELIST))
38600 (COND ((AND Z1 Z2) (SETQ RF NIL) (GO URE1A)) (T (GO U3A)))
38700 USI1 (COND ((NULL (SETQ Z1 (UPGETL E NAMELIST))) (GO U3A)))
38800 (COND ((NOT (EQ (READ) (QUOTE BY))) (GO UER2)))
38900 (COND ((NULL (SETQ Z2 (UPGETL E NAMELIST))) (GO U3A)))
39000 (SETQ Z3 Z1)
39100 (SETQ Z DDEPTH)
39200 (SETQ DDEPTH 22)
39300 USI2 (DEMOD (LIST (CAR Z3)) Z2)
39400 (SETQ Z3 (CDR Z3))
39500 (COND (Z3 (GO USI2)))
39600 (PRINT (QUOTE CLAUSES-ARE:))
39700 (CLAUSES Z1)
39800 (SETQ DDEPTH Z)
39900 (GO U3A)
40200 UCU1 (QUERY)
40300 (GO U3A)
40400 UDS1 (SETQ Z1 (READ))
40500 (COND ((NOT (ATOM Z1)) (GO UDS3)))
40600 UDS2 (COND
40700 ((EQ (CAR (SETQ Z2 (REVERSE (EXPLODE Z1)))) (QUOTE ;)) (SETQ Z1 (READLIST (REVERSE (CDR Z2))))
40800 (GO UDS2)))
40900 UDS3 (SETQ CHAN1 (EVAL (LIST (QUOTE OUTC) (LIST (QUOTE OUTPUT) (QUOTE EDIT) (QUOTE DSK:) Z1) NIL)))
41000 (GO U3A)
41100 UEO1 (OUTC CHAN1 T)
41200 (GO U3A)
41300 UUS1 (SETQ NAME (QUOTE %USING))
41400 (SETQ USINGFL T)
41500 (SETQ USING NIL)
41600 UUS3 (SETQ LOCFLG T)
41700 UUS2 (SETQ Z2 (UPGETL E NAMELIST))
41800 (SETQ USINGFL NIL)
41900 (COND ((NULL Z2) (GO U3A)))
42000 USE2 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) (RPLACD Z1 Z2)))
42100 (COND (LOCFLG (RPLACD NAMELIST (CONS (CONS NAME Z2) (CDR NAMELIST))))
42200 (T (RPLACA (CAR N1) NAME)
42300 (RPLACD (CAR N1) Z2)
42400 (RPLACD N1 (CONS (CONS NIL NIL) NIL))
42500 (SETQ N1 (CDR N1))))
42600 (GO U3A)
42700 USE1 (SETQ NAME (READ))
42800 (SETQ LOCFLG NIL)
42900 (GO UUS2)
43000 UCL1 (SETQ Z (READ))
43100 UCL2 (COND ((SETQ Z1 (ASSOC Z NAMELIST)) (RPLACA Z1 (QUOTE %%)) (GO U3A))
43200 ((EQ (CAR (SETQ Z (REVERSE (EXPLODE Z)))) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z))))
43300 (GO UCL2))
43400 (T (GO U3A)))
43500 UGO1 (SETQ Z1 (READ))
43600 (COND ((NOT (NUMBERP Z1)) (GO UER2)))
43700 (COND ((SETQ Z (DOWN Z1 E)) (SETQ ELOC Z) (SETQ N Z1) (GO U3))
43800 (T (PRINT (QUOTE NO-SUCH-CLAUSE)) (GO U3A)))
43900 UTR1 (SETQ UEX NIL)
44000 (GO UEX2)
44100 UEX1 (SETQ UEX T)
44200 UEX2 (SETQ NAME (QUOTE LEMMA))
44300 (SETQ XYZ (GETNAME (QUOTE NEGLEMMA) NAMELIST))
44400 (COND ((NULL XYZ) (PRINT (QUOTE NOTHING-TO-PROVE)) (GO U3A)))
44500 (SETQ AUTO T)
44600 (SETQ Z2
44700 (ATTEMPT (INITIALAX (CONS (QUOTE THEOREM) (APPEND XYZ USING)))
44800 (COND (UEX (RESET (DLIST (GETNAME (QUOTE DLIST) NAMELIST)) (STRATEGY (SUPPORT XYZ))))
44900 (T NIL))
45000 NIL))
45100 (SETQ AUTO NIL)
45200 (GO AT1A)
45300 UST1 (STOP)
45400 (GO U3A)
45500 UAB1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z1 NIL)) (T (SETQ Z1 (UPGETL E NAMELIST))))
45600 (ERR (CONS (QUOTE ABORT) (CONS Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))))
45700 U8 (COND ((EQ Z2 0) (GO U9)))
45800 U83 (COND ((NULL Z2) (GO U3A)) ((TTYIN) (GO U3A)) ((LESSP Z2 5) (SETQ ZZ Z2) (SETQ Z2 NIL) (GO U84)))
45900 (SETQ Z2 (DIFFERENCE Z2 5))
46000 (SETQ ZZ 5)
46100 U84 (SETQ Z N)
46200 (SETQ Z3 (DIFFERENCE N ZZ))
46300 (COND ((OR (ZEROP Z3) (MINUSP Z3)) (SETQ Z3 1) (SETQ Z2 NIL)))
46400 (SETQ N Z3)
46500 (SETQ Z3 ELOC)
46600 (SETQ ELOC (DOWN N E))
46700 (SETQ ZZ NIL)
46800 (SETQ Z1 ELOC)
46900 U81 (COND ((EQ Z1 Z3) (GO U82)))
47000 (SETQ ZZ (CONS (CAR Z1) ZZ))
47100 (SETQ Z1 (CDR Z1))
47200 (GO U81)
47300 U82 (COND ((NULL ZZ) (GO U83)))
47400 (UP1A (CAR ZZ) (SUB1 Z))
47500 (SETQ ZZ (CDR ZZ))
47600 (SETQ Z (SUB1 Z))
47700 (GO U82)
47800 U7 (COND ((ZEROP Z2) (SETQ ELOC (LAST ELOC)) (SETQ N (LENGTH E)) (GO U3)))
47900 (SETQ Z2 (PLUS Z2 N))
48000 U7A (COND ((NULL (CDR ELOC)) (PRINT (QUOTE END)) (GO U3A)))
48100 (SETQ ELOC (CDR ELOC))
48200 (SETQ N (ADD1 N))
48300 (UP1A (CAR ELOC) N)
48400 (COND ((EQ N Z2) (GO U3A)) ((TTYIN) (GO U3A)) (T (GO U7A)))
48500 UPR1 (TERPRI)
48600 (SETQ XYZ NIL)
48700 (SETQ Z2 (UPGETL E NAMELIST))
48800 (COND ((NULL Z2) (PRINT (QUOTE NO-CLAUSES-GIVEN)) (GO U3A)))
48900 (COND ((GREATERP (LENGTH Z2) 1) (PRINT (QUOTE MORE-THAN-ONE-CLAUSE-TAKING-THE-FIRST-ONE))))
49000 (SETQ AXNO (QUOTE THEOREM))
49100 (SETQ Z3 (COND ((NULL XYZ) (NEGATE (CDAR Z2))) (T (SET3 (SETUP (CNF (LIST (QUOTE NOT) XYZ)))))))
49200 (SETQ AXNO (QUOTE INSERT))
49300 (SETQ Z1 (ASSOC (QUOTE NEGLEMMA) NAMELIST))
49400 (COND (Z1 (RPLACD Z1 Z3)) (T (RPLACD NAMELIST (CONS (CONS (QUOTE NEGLEMMA) Z3) (CDR NAMELIST)))))
49500 (SETQ NAME (QUOTE LEMMA))
49600 (SETQ LOCFLG T)
49700 (GO USE2)
49800 UME1 (SETQ Z1 (UPGETL E NAMELIST))
49900 (SETQ Z2 (UPGETL E NAMELIST))
50000 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
50100 (BAKSUB Z1 Z2)
50200 (GO U3A)
50300 UHE1 (PRINT MESSAGE)
50400 (GO U3A)
50500 URE1 (SETQ Z1 (UPGETL E NAMELIST))
50600 (SETQ Z2 (UPGETL E NAMELIST))
50700 U%RE1
50800 (SETQ RF T)
50900 URE1A
51000 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
51100 (SETQ Z1R Z1)
51200 (SETQ Z2R Z2)
51300 (SETQ Z3 NIL)
51400 (COND ((OR (NULL Z1) (NULL Z2)) (GO UR3B)))
51500 (COND ((NOT RF) (SETQ DL1 DLIST) (SETQ DLIST NIL)))
51600 UR3 (COND ((AND RF (ALLPOS (CAR Z1R)) (ALLPOS (CAR Z2R))) (GO UR3A))
51700 ((AND (ALLNEG (CAR Z1R)) (ALLNEG (CAR Z2R))) (GO UR3A)))
51800 (COND (RF (SETQ R (RESOLVE (CAR Z1R) (CAR Z2R)))) (T (SETQ R (PARMOD (CAR Z1R) (CAR Z2R)))))
51900 (COND ((NULL R) (GO UR3A)) ((MEMQ NIL R) (PROOF (CAR Z1R) (CAR Z2R)) (GO U3A)))
52000 (SETQ Z3 (BOOKEEP Z3 R (CONS (CAR Z1R) (CAR Z2R))))
52100 UR3A (SETQ Z2R (CDR Z2R))
52200 (COND (Z2R (GO UR3)))
52300 (SETQ Z1R (CDR Z1R))
52400 (COND (Z1R (SETQ Z2R Z2) (GO UR3)))
52500 UR3B (COND ((NULL Z3)
52600 (COND (RF (PRINT (QUOTE NO-RESOLVENTS)) (GO U3A))
52700 (T (PRINT (QUOTE NO-PARMODULANTS)) (SETQ DLIST DL1) (GO U3A))))
52800 (RF (SETQ NAME (QUOTE RES)))
52900 (T (SETQ NAME (QUOTE PAR)) (SETQ DLIST DL1)))
53000 (SETQ Z2 Z3)
53100 (SETQ LOCFLG T)
53200 (GO AT2A)
53300 UEV1 (PRINT (QUOTE EVAL-AWAITS))
53400 (SETQ Z2 (ERRSET (EVAL (READ)) T))
53500 (COND (Z2 (PRINT (CAR Z2)) (GO UE2)) (T (PRINT (QUOTE LOSE)) (GO UEV1)))
53600 UE2 (COND ((EQ (QUOTE END) (CAR Z2)) (GO U3A)))
53700 (GO UEV1)
53800 AT1A (UPDATESTATE STRAT)
53900 (COND
54000 ((OR (NULL Z2) (AND (EQ (CAR Z2) (QUOTE ABORT)) (NULL (CADR Z2))))
54100 (PRINT (QUOTE ATTEMPT-ABORTED-FOR:))
54200 (PRINC NAME)
54300 (GO U3A))
54400 ((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ AUTO T)
54500 (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL))
54600 (SETQ AUTO NIL)
54700 (GO AT1A))
54800 ((EQ (CAR Z2) (QUOTE QED)) (PRINT (QUOTE PROOF-FOUND-FOR:)) (PRINC NAME) (GO U3A)))
54900 (SETQ Z2 (CADR Z2))
55000 AT2A (SETQ N 1)
55100 AT2 (COND ((ASSOC (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))) NAMELIST) (SETQ N (ADD1 N)) (GO AT2)))
55200 (SETQ NAME (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))))
55300 (PRINT (QUOTE THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES:))
55400 (PRINT (QUOTE THEY-WILL-BE-FOUND-UNDER-THE-NAME:))
55500 (PRIN1 NAME)
55600 (CLAUSES Z2)
55700 (GO USE2)))
55800 EXPR)
55900
56000 (DEFPROP UPGETL
56100 (LAMBDA(E N)
56200 (PROG (C)
56300 (SCANSET)
56400 (START)
56500 (SETQ C (ERRSET (<CLAUSES>) T))
56600 (SCANRESET)
56700 (COND ((OR (NULL C) (NULL (CAR C))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
56800 (SETQ C (TOP))
56900 (COND ((EQ C (QUOTE EMPTY)) (RETURN NIL)))
57000 (RETURN (UPGETL1 C E N))))
57100 EXPR)
57200
57300 (DEFPROP UPGETL1
57400 (LAMBDA(C E N)
57500 (PROG (N1 Z Z1 Z2 Z3 ZZ N2)
57600 AS1 (SETQ Z (CAR C))
57700 (COND ((ATOM Z)
57800 (COND ((NUMBERP Z) (SETQ N2 (QUOTE CLAUSES))
57900 (COND ((SETQ Z1 (DOWN Z E)) (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1)))))
58000 (T (RETURN NIL))))
58100 ((SETQ Z1 (GETNAME Z N)) (SETQ N2 Z) (SETQ ZZ (APPENDIT ZZ Z1)))
58200 (T (RETURN NIL))))
58300 ((EQ (CAR Z) (QUOTE STAT)) (GO AS10))
58400 ((EQ (CAR Z) (QUOTE FIND)) (GO AS20))
58500 ((EQ (CAR Z) (QUOTE DSK)) (GO AS30))
58600 ((SETQ Z1 (GETNAME (CAR Z) N)) (SETQ N2 (CAR Z)) (GO AS2))
58700 (T (RETURN NIL)))
58800 AS6 (SETQ C (CDR C))
58900 (COND (C (GO AS1)) (T (RETURN ZZ)))
59000 AS2 (SETQ Z2 (CADR Z))
59100 (SETQ N1 (CAR Z))
59200 (SETQ Z (CDR Z))
59300 (SETQ Z3 Z1)
59400 AS2A (COND ((NOT (NUMBERP Z2)) (PRINT (QUOTE NON-NUMERIC-ARG-FOR:)) (PRINC N1) (RETURN NIL)))
59500 AS3 (SETQ Z2 (SUB1 Z2))
59600 (COND ((ZEROP Z2) (GO AS4)))
59700 (SETQ Z1 (CDR Z1))
59800 (COND (Z1 (GO AS3)) (T (PRINT (QUOTE EXCEEDED-SIZE-OF:)) (PRINC N1) (RETURN NIL)))
59900 AS4 (COND
60000 ((NOT (HERE (CAR Z1))) (PRINT N1)
60100 (PRINC (QUOTE / ))
60200 (PRINC (CAR Z))
60300 (PRINC (QUOTE / ))
60400 (PRINC (QUOTE HAS-BEEN-DELETED))
60500 (RETURN NIL)))
60600 (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1))))
60700 (SETQ Z (CDR Z))
60800 (COND (Z (SETQ Z1 Z3) (SETQ Z2 (CAR Z)) (GO AS2A)))
60900 (GO AS6)
61000 AS10 (SETQ N2 (QUOTE INSERT))
61100 (SETQ ZZ (APPENDIT ZZ (SET3 (SETUP (CNF (SETQ XYZ (FIXQFF (CDR Z))))))))
61200 (GO AS6)
61300 AS20 (SETQ N2 (QUOTE MATCHES))
61400 (SETQ Z (MAPIT (CADR Z) (LIST (QUOTE FUNCTION) (LIST (QUOTE LAMBDA) (QUOTE (C)) (CADDR Z))) N))
61500 (COND ((NULL Z) (GO AS6)) (T (GO AS31)))
61600 AS30 (SETQ N2 (QUOTE INPUT))
61700 (SETQ ZIN (CDR Z))
61800 (COND
61900 ((NULL (ERRSET (EVAL (LIST (QUOTE INPUT) (QUOTE DSK:) ZIN)))) (PRINT (QUOTE CONTINUING)) (GO AS6)))
62000 (INC T)
62100 (SETQ Z (INCLAUSES))
62200 (INC NIL)
62300 (COND ((NULL Z) (RETURN NIL)))
62400 AS31 (SETQ ZZ (APPENDIT ZZ Z))
62500 (GO AS6)))
62600 EXPR)
62700
62800 (DEFPROP UPGETNU
62900 (LAMBDA NIL (PROG (Z) (SETQ Z (READ)) (COND ((NUMBERP Z) (READ) (RETURN Z)) (T (RETURN NIL)))))
63000 EXPR)
63100
63200 (DEFPROP UPDATESTATE
63300 (LAMBDA(L)
63400 (PROG (L1)
63500 (SETQ L1 STATEVECTOR)
63600 A (COND ((NULL L) (RETURN NIL)))
63700 (SET (CAR L1) (CAR L))
63800 (SETQ L (CDR L))
63900 (SETQ L1 (CDR L1))
64000 (GO A)))
64100 EXPR)
64200
64300 (DEFPROP UPIT
64400 (LAMBDA (C) (COND ((NEG C) (UPIT1 (CDDR C))) (T (UPIT1 (CDR C)))))
64500 EXPR)
64600
64700 (DEFPROP UPIT1
64800 (LAMBDA(Z)
64900 (PROG (Z1 Z2)
65000 MAX2 (SETQ Z2 (CAR Z))
65100 (COND ((VAR Z2) (COND ((SETQ Z1 (ASSOC Z2 BL)) (RPLACA Z (CDR Z1)))
65200 ((GREATERP Z2 NO*) NIL)
65300 (T (SETQ BL (CONS (CONS Z2 (SETQ NO (ADD1 NO))) BL)) (RPLACA Z NO)))
65400 (GO MAX1))
65500 ((CONST Z2) (GO MAX1))
65600 (T (UPIT1 (CDR Z2))))
65700 MAX1 (SETQ Z (CDR Z))
65800 (COND (Z (GO MAX2)))
65900 (RETURN NO)))
66000 EXPR)
66100
66200 (DEFPROP UP1A
66300 (LAMBDA(X N)
66400 (PROG NIL
66500 (TERPRI)
66600 (PRINC N)
66700 (PRINC (QUOTE / ))
66800 (COND ((HERE X) (PRFPRINT (CDR X))) (T (PRINC (QUOTE *DE*))))
66900 (RETURN NIL)))
67000 EXPR)
67100
67200 (DEFPROP UP1B
67300 (LAMBDA (X N) (PROG NIL (TERPRI) (PRINC N) (PRINC (QUOTE / )) (PRFPRINT (CDR X))))
67400 EXPR)
67500
67600 (DEFPROP VARIT
67700 (LAMBDA(Z)
67800 (PROG (Z1 Z2 BL Z3)
67900 (SETQ Z3 Z)
68000 M1 (SETQ Z2 (CAR Z))
68100 (COND ((VAR Z2)
68200 (COND ((SETQ Z1 (ASSOC Z2 BL)) (RPLACA Z (CDR Z1)))
68300 (T (SETQ BL (CONS (CONS Z2 (SETQ NO (ADD1 NO))) BL)) (RPLACA Z NO))))
68400 ((EQ (CAR Z2) (QUOTE _)) (RPLACA Z (SETQ NO (ADD1 NO))))
68500 ((CONST Z2) NIL)
68600 (T (VARIT (CDR Z2))))
68700 (SETQ Z (CDR Z))
68800 (COND (Z (GO M1)))
68900 (RETURN Z3)))
69000 EXPR)
69100
69200 (DEFPROP VINE
69300 (LAMBDA (X) (NUMBERP (CDR (ANCESTOR X))))
69400 EXPR)
69500
69600 (DEFPROP <
69700 (LAMBDA(L X)
69800 (PROG (Z Z1 Z2)
69900 (SETQ Z X)
70000 (COND ((NEG L) (SETQ L (CADR L)) (SETQ Z2 T)) (T (SETQ L (CAR L))))
70100 A1 (SETQ Z1 (CAR Z))
70200 (COND ((NEG Z1) (SETQ Z1 (CADR Z1))) (T (SETQ Z1 (CAR Z1))))
70300 (COND ((NOT (ORDERP L Z1)) (GO A2))
70400 ((OR (AND (NOT Z2) (MEMBER Z1 PMODEL)) (AND Z2 (MEMBER Z1 NMODEL))) (RETURN T)))
70500 A2 (SETQ Z (CDR Z))
70600 (COND (Z (GO A1)))
70700 (RETURN NIL)))
70800 EXPR)
00100
00110 (DE MAXLENGTH(X N)(GREATERP (NUM X) N))
00120
00200
00300 (DEFPROP MAXDEPTH
00400 (LAMBDA(Z N)
00500 (PROG NIL
00600 D1 (COND ((MAXDEPTH1 (COND ((NEG (CAR Z)) (CDDAR Z)) (T (CDAR Z))) N) (RETURN T)))
00700 (SETQ Z (CDR Z))
00800 (COND (Z (GO D1)) (RETURN NIL))))
00900 EXPR)
01000
01100 (DEFPROP MAXDEPTH1
01200 (LAMBDA(Z N)
01300 (PROG NIL
01400 D1 (COND ((OR (VAR (CAR Z)) (CONST (CAR Z))) (GO D2))
01500 ((EQ N 1) (RETURN T))
01600 ((MAXDEPTH1 (CDAR Z) (SUB1 N)) (RETURN T)))
01700 D2 (SETQ Z (CDR Z))
01800 (COND (Z (GO D1)))
01900 (RETURN NIL)))
02000 EXPR)